fof(l85_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & v1_anproj_2(A) & l2_rlvect_1(A) ) => v6_anproj_2(k6_anproj_1(A)) ) ), inference(mizar_proof,[status(thm)],[d13_anproj_2,t24_anproj_2,t24_anproj_2,t35_anproj_1,t9_anproj_1,t24_anproj_2,t35_anproj_1,t9_anproj_1,t24_anproj_2,t35_anproj_1,t9_anproj_1,t24_anproj_2,d4_anproj_2,t35_anproj_1,d5_anproj_2,d1_anproj_2,t24_anproj_2,t35_anproj_1,t9_anproj_1,t24_anproj_2,t35_anproj_1,t9_anproj_1,t24_anproj_2,t35_anproj_1,t9_anproj_1,t24_anproj_2,t35_anproj_1,t9_anproj_1,t24_anproj_2,t35_anproj_1,t9_anproj_1,t24_anproj_2,t35_anproj_1,t9_anproj_1,d1_anproj_2,t9_anproj_2,t24_anproj_2]), [file(anproj_2,l85_anproj_2),interesting(1.00)]). fof(l84_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & v1_anproj_2(A) & l2_rlvect_1(A) ) => v5_anproj_2(k6_anproj_1(A)) ) ), inference(mizar_proof,[status(thm)],[d12_anproj_2,t42_anproj_1,t24_anproj_2,t24_anproj_2,t35_anproj_1,t9_anproj_1,t24_anproj_2,t35_anproj_1,t9_anproj_1,t24_anproj_2,t35_anproj_1,t9_anproj_1,t24_anproj_2,t35_anproj_1,t9_anproj_1,t24_anproj_2,t35_anproj_1,t9_anproj_1,t35_anproj_1,t24_anproj_2,t35_anproj_1,t9_anproj_1,t24_anproj_2,t35_anproj_1,t9_anproj_1,t24_anproj_2,t35_anproj_1,t9_anproj_1,d1_anproj_2,d1_anproj_2,d1_anproj_2,d3_anproj_2,t24_anproj_2,t24_anproj_2,t24_anproj_2,d2_anproj_2,d2_anproj_2,t8_anproj_2,t24_anproj_2]), [file(anproj_2,l84_anproj_2),interesting(0.99)]). fof(l74_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & ~ v3_realset2(A) & l2_rlvect_1(A) ) => ( v1_anproj_2(A) => v3_anproj_2(k6_anproj_1(A)) ) ) ), inference(mizar_proof,[status(thm)],[d6_anproj_2,t10_rlvect_1,t23_rlvect_1,t26_anproj_2]), [file(anproj_2,l74_anproj_2),interesting(0.75)]). fof(l72_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & ~ v3_realset2(A) & l2_rlvect_1(A) ) => ( v1_anproj_2(A) => v4_collsp(k6_anproj_1(A)) ) ) ), inference(mizar_proof,[status(thm)],[d6_anproj_2,t1_anproj_2,t1_anproj_2,t42_anproj_1,d6_collsp,d2_collsp,t41_anproj_1]), [file(anproj_2,l72_anproj_2),interesting(0.71)]). fof(l71_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & ~ v3_realset2(A) & l2_rlvect_1(A) ) => v2_anproj_2(k6_anproj_1(A)) ) ), inference(mizar_proof,[status(thm)],[d9_anproj_2,l69_anproj_2,l70_anproj_2]), [file(anproj_2,l71_anproj_2),interesting(0.70)]). fof(l67_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & ~ v3_realset2(A) & l2_rlvect_1(A) ) => v3_collsp(k6_anproj_1(A)) ) ), inference(mizar_proof,[status(thm)],[d8_anproj_2,t42_anproj_1,t42_anproj_1,t24_anproj_2,t24_anproj_2,t24_anproj_2,t35_anproj_1,t35_anproj_1,t9_anproj_1,t19_anproj_1,t24_anproj_2]), [file(anproj_2,l67_anproj_2),interesting(0.65)]). fof(l83_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & v1_anproj_2(A) & l2_rlvect_1(A) ) => v4_anproj_2(k6_anproj_1(A)) ) ), inference(mizar_proof,[status(thm)],[t28_anproj_2,d11_anproj_2]), [file(anproj_2,l83_anproj_2),interesting(0.64)]). fof(t9_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ! [H] : ( m1_subset_1(H,u1_struct_0(A)) => ! [I] : ( m1_subset_1(I,u1_struct_0(A)) => ! [J] : ( m1_subset_1(J,u1_struct_0(A)) => ! [K] : ( m1_subset_1(K,u1_struct_0(A)) => ( ( v8_rlvect_1(B,A) & r1_anproj_2(A,C,D,E) & r1_anproj_2(A,F,G,H) & r1_anproj_2(A,I,J,K) & r4_anproj_2(A,B,C,D,E,F,G,H) & r5_anproj_2(A,B,C,D,E,F,G,H) & r2_anproj_1(A,C,G,K) & r2_anproj_1(A,F,D,K) & r2_anproj_1(A,C,H,J) & r2_anproj_1(A,E,F,J) & r2_anproj_1(A,D,H,I) & r2_anproj_1(A,E,G,I) ) => r2_anproj_1(A,I,J,K) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_anproj_2,d4_anproj_2,d5_anproj_2,t17_anproj_1,d1_anproj_2,t6_anproj_2,t6_anproj_2,t6_anproj_2,t6_anproj_2,l29_anproj_2,t6_anproj_1,t6_anproj_1,t6_anproj_1,t6_anproj_1,t9_anproj_1,t10_anproj_1,t9_anproj_1,t9_anproj_1,t10_anproj_1,t9_anproj_1,t10_anproj_1,t10_anproj_1,t16_anproj_1,t19_anproj_1,t9_anproj_1,t10_anproj_1,t10_anproj_1,t16_anproj_1,t19_anproj_1,t9_anproj_1,t9_anproj_1,t10_anproj_1,l33_anproj_2,l30_anproj_2,l30_anproj_2,t9_anproj_1,t9_anproj_1,l30_anproj_2,l30_anproj_2,t11_anproj_1,t11_anproj_1,l31_anproj_2,l32_anproj_2,t13_anproj_1,t23_rlvect_1,t23_rlvect_1,t10_rlvect_1,d13_rlvect_1,l42_anproj_2,l29_anproj_2,t11_anproj_1,t11_anproj_1,l31_anproj_2,l32_anproj_2,t13_anproj_1,t23_rlvect_1,t23_rlvect_1,t10_rlvect_1,d13_rlvect_1,l42_anproj_2,l29_anproj_2,l34_anproj_2,l34_anproj_2,t9_anproj_1,t11_anproj_1,t11_anproj_1,l35_anproj_2,l35_anproj_2,t13_anproj_1,l37_anproj_2,l39_anproj_2,t23_rlvect_1,t23_rlvect_1,t10_rlvect_1,d13_rlvect_1,l38_anproj_2,l29_anproj_2,l41_anproj_2,d3_anproj_1,t9_anproj_1]), [file(anproj_2,t9_anproj_2),interesting(0.63)]). fof(t8_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ! [H] : ( m1_subset_1(H,u1_struct_0(A)) => ! [I] : ( m1_subset_1(I,u1_struct_0(A)) => ! [J] : ( m1_subset_1(J,u1_struct_0(A)) => ! [K] : ( m1_subset_1(K,u1_struct_0(A)) => ( ( v8_rlvect_1(B,A) & r1_anproj_2(A,C,D,E) & r1_anproj_2(A,F,G,H) & r1_anproj_2(A,I,J,K) & r3_anproj_2(A,B,C,D,E,F,G,H) & r2_anproj_2(A,C,D,E,I,J,K) & r2_anproj_2(A,F,G,H,I,J,K) ) => ( r1_anproj_1(A,B,F) | r1_anproj_1(A,B,G) | r1_anproj_1(A,B,H) | r1_anproj_1(A,C,F) | r1_anproj_1(A,D,G) | r1_anproj_1(A,E,H) | r2_anproj_1(A,B,C,D) | r2_anproj_1(A,B,C,E) | r2_anproj_1(A,B,D,E) | r2_anproj_1(A,I,J,K) ) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_anproj_2,d3_anproj_2,d2_anproj_2,t16_anproj_1,d1_anproj_2,t6_anproj_2,t6_anproj_2,t6_anproj_2,d1_anproj_2,t17_anproj_1,t7_anproj_2,t7_anproj_2,t7_anproj_2,l19_anproj_2,t9_anproj_1,l20_anproj_2,l21_anproj_2,d1_anproj_2,t7_anproj_2,t7_anproj_2,t7_anproj_2,l22_anproj_2,l23_anproj_2,t13_anproj_1,l24_anproj_2,d13_rlvect_1,l24_anproj_2,d13_rlvect_1,l24_anproj_2,d13_rlvect_1,l25_anproj_2,l19_anproj_2,d9_rlvect_1,d9_rlvect_1,t29_rlvect_1,t47_rlvect_1,d11_rlvect_1,d11_rlvect_1,d6_rlvect_1,d6_rlvect_1,t16_rlvect_1,t10_rlvect_1,d6_rlvect_1,d6_rlvect_1,t16_rlvect_1,t10_rlvect_1,t16_rlvect_1,d3_anproj_1,t9_anproj_1]), [file(anproj_2,t8_anproj_2),interesting(0.58)]). fof(l50_anproj_2,theorem,( ? [A] : ( ~ v1_xboole_0(A) & ? [B] : ( m1_subset_1(B,A) & ? [C] : ( m1_subset_1(C,A) & ? [D] : ( m1_subset_1(D,A) & A = k8_domain_1(A,B,C,D) & B != C & B != D & C != D ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_enumset1,d1_enumset1]), [file(anproj_2,l50_anproj_2),interesting(0.58)]). fof(l66_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & ~ v3_realset2(A) & l2_rlvect_1(A) ) => v2_collsp(k6_anproj_1(A)) ) ), inference(mizar_proof,[status(thm)],[d7_anproj_2,t42_anproj_1,t42_anproj_1,t16_anproj_1,t24_anproj_2]), [file(anproj_2,l66_anproj_2),interesting(0.57)]). fof(l36_anproj_2,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,k1_numbers) => ~ ( A != B & C != 0 & k5_real_1(k4_real_1(B,C),k4_real_1(A,C)) = 0 ) ) ) ) ), inference(mizar_proof,[status(thm)],[t6_xcmplx_1]), [file(anproj_2,l36_anproj_2),interesting(0.57)]). fof(l58_anproj_2,theorem,( ? [A] : ( ~ v1_xboole_0(A) & ? [B] : ( m1_subset_1(B,A) & ? [C] : ( m1_subset_1(C,A) & ? [D] : ( m1_subset_1(D,A) & ? [E] : ( m1_subset_1(E,A) & A = k9_domain_1(A,B,C,D,E) & B != C & B != D & B != E & C != D & C != E & D != E ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_enumset1,d2_enumset1]), [file(anproj_2,l58_anproj_2),interesting(0.56)]). fof(t7_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ~ ( r2_anproj_1(A,B,C,D) & ~ r1_anproj_1(A,B,C) & r1_anproj_2(A,B,C,D) & ! [E] : ( m1_subset_1(E,k1_numbers) => ! [F] : ( m1_subset_1(F,k1_numbers) => D != k4_rlvect_1(A,k3_rlvect_1(A,B,E),k3_rlvect_1(A,C,F)) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_anproj_2,d13_rlvect_1,d3_anproj_1,t23_rlvect_1,t23_rlvect_1,t10_rlvect_1,t10_rlvect_1,t24_rlvect_1,t23_rlvect_1,t23_rlvect_1,t10_rlvect_1,t10_rlvect_1,t24_rlvect_1,t23_rlvect_1,t10_rlvect_1,t19_rlvect_1,l16_anproj_2,d2_anproj_1,d10_rlvect_1,t45_rlvect_1,l16_anproj_2,l16_anproj_2,d9_rlvect_1,d9_rlvect_1,d9_rlvect_1,d9_rlvect_1,d7_xcmplx_0,d9_rlvect_1]), [file(anproj_2,t7_anproj_2),interesting(0.52)]). fof(t26_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & ~ v3_realset2(A) & l2_rlvect_1(A) ) => ( ? [B] : ( m1_subset_1(B,u1_struct_0(A)) & ? [C] : ( m1_subset_1(C,u1_struct_0(A)) & ! [D] : ( m1_subset_1(D,k1_numbers) => ! [E] : ( m1_subset_1(E,k1_numbers) => ( k4_rlvect_1(A,k3_rlvect_1(A,B,D),k3_rlvect_1(A,C,E)) = k1_rlvect_1(A) => ( D = 0 & E = 0 ) ) ) ) ) ) => v3_anproj_2(k6_anproj_1(A)) ) ) ), inference(mizar_proof,[status(thm)],[d10_anproj_2,t42_anproj_1,t42_anproj_1,l2_anproj_2,l2_anproj_2,t21_anproj_1,t42_anproj_1,t35_anproj_1,t35_anproj_1,t24_anproj_2]), [file(anproj_2,t26_anproj_2),interesting(0.44)]). fof(l2_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( ! [D] : ( m1_subset_1(D,k1_numbers) => ! [E] : ( m1_subset_1(E,k1_numbers) => ( k4_rlvect_1(A,k3_rlvect_1(A,B,D),k3_rlvect_1(A,C,E)) = k1_rlvect_1(A) => ( D = 0 & E = 0 ) ) ) ) => ( v8_rlvect_1(B,A) & v8_rlvect_1(C,A) & ~ r1_anproj_1(A,B,C) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d13_rlvect_1,t10_rlvect_1,d9_rlvect_1,t23_rlvect_1,d13_rlvect_1,t10_rlvect_1,d9_rlvect_1,t23_rlvect_1,d2_anproj_1,t28_rlvect_1,d11_rlvect_1,t39_rlvect_1,t38_rlvect_1]), [file(anproj_2,l2_anproj_2),interesting(0.43)]). fof(t33_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & ~ v3_realset2(A) & l2_rlvect_1(A) ) => ~ ( v4_collsp(k6_anproj_1(A)) & v3_anproj_2(k6_anproj_1(A)) & ? [B] : ( m1_subset_1(B,u1_struct_0(k6_anproj_1(A))) & ? [C] : ( m1_subset_1(C,u1_struct_0(k6_anproj_1(A))) & ? [D] : ( m1_subset_1(D,u1_struct_0(k6_anproj_1(A))) & ~ r1_collsp(k6_anproj_1(A),B,C,D) & ! [E] : ( m1_subset_1(E,u1_struct_0(k6_anproj_1(A))) => ! [F] : ( m1_subset_1(F,u1_struct_0(k6_anproj_1(A))) => ? [G] : ( m1_subset_1(G,u1_struct_0(k6_anproj_1(A))) & ? [H] : ( m1_subset_1(H,u1_struct_0(k6_anproj_1(A))) & r1_collsp(k6_anproj_1(A),E,F,H) & r1_collsp(k6_anproj_1(A),C,D,G) & r1_collsp(k6_anproj_1(A),B,H,G) ) ) ) ) ) ) ) & ! [B] : ( ( ~ v3_struct_0(B) & v2_collsp(B) & v3_collsp(B) & v4_collsp(B) & v2_anproj_2(B) & v3_anproj_2(B) & l1_collsp(B) ) => ~ ( B = k6_anproj_1(A) & v8_anproj_2(B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d10_anproj_2,d7_anproj_2,d7_anproj_2,d7_anproj_2,t25_anproj_2,d7_anproj_2,d8_anproj_2,d7_anproj_2,d7_anproj_2,d7_anproj_2,d7_anproj_2,d7_anproj_2,d7_anproj_2,d7_anproj_2,d7_anproj_2,d8_anproj_2,t25_anproj_2,t25_anproj_2,d7_anproj_2,d8_anproj_2,t25_anproj_2,d9_anproj_2,d7_anproj_2,d8_anproj_2,d8_anproj_2,t25_anproj_2,t25_anproj_2,d7_anproj_2,d8_anproj_2,d7_anproj_2,d8_anproj_2,d8_anproj_2,l92_anproj_2,t25_anproj_2,d9_anproj_2,t25_anproj_2,d9_anproj_2,d7_anproj_2,d8_anproj_2,d8_anproj_2,d7_anproj_2,d8_anproj_2,d8_anproj_2,t25_anproj_2,d7_anproj_2,d7_anproj_2,t25_anproj_2,d8_anproj_2,t25_anproj_2,d9_anproj_2,d7_anproj_2,d7_anproj_2,d8_anproj_2,d8_anproj_2,t19_collsp,t25_anproj_2,d7_anproj_2,t25_anproj_2,d8_anproj_2,d7_anproj_2,t25_anproj_2,t25_anproj_2,d10_anproj_2,d15_anproj_2]), [file(anproj_2,t33_anproj_2),interesting(0.41)]). fof(t6_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( ( r2_anproj_1(A,B,C,D) & r1_anproj_2(A,B,C,D) ) => ( r1_anproj_1(A,B,C) | r1_anproj_1(A,B,D) | r1_anproj_1(A,C,D) | ( ? [E] : ( m1_subset_1(E,k1_numbers) & ? [F] : ( m1_subset_1(F,k1_numbers) & k3_rlvect_1(A,D,F) = k4_rlvect_1(A,B,k3_rlvect_1(A,C,E)) & E != 0 & F != 0 ) ) & ? [E] : ( m1_subset_1(E,k1_numbers) & ? [F] : ( m1_subset_1(F,k1_numbers) & D = k4_rlvect_1(A,k3_rlvect_1(A,B,F),k3_rlvect_1(A,C,E)) & F != 0 & E != 0 ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_anproj_1,d1_anproj_2,d13_rlvect_1,t23_rlvect_1,t10_rlvect_1,t23_rlvect_1,t10_rlvect_1,t24_rlvect_1,t23_rlvect_1,t10_rlvect_1,t23_rlvect_1,t10_rlvect_1,t24_rlvect_1,t23_rlvect_1,t10_rlvect_1,t19_rlvect_1,t39_rlvect_1,t38_rlvect_1,d2_anproj_1,t23_rlvect_1,t10_rlvect_1,t23_rlvect_1,t10_rlvect_1,t24_rlvect_1,t23_rlvect_1,t10_rlvect_1,t23_rlvect_1,t10_rlvect_1,t24_rlvect_1,t23_rlvect_1,t10_rlvect_1,t19_rlvect_1,t39_rlvect_1,t38_rlvect_1,d2_anproj_1,t23_rlvect_1,t10_rlvect_1,t23_rlvect_1,t10_rlvect_1,t24_rlvect_1,t23_rlvect_1,t10_rlvect_1,t23_rlvect_1,t10_rlvect_1,t24_rlvect_1,t23_rlvect_1,t10_rlvect_1,t19_rlvect_1,t39_rlvect_1,t38_rlvect_1,d2_anproj_1,t19_rlvect_1,d9_rlvect_1,d9_rlvect_1,d9_rlvect_1,d7_xcmplx_0,d9_rlvect_1,t39_rlvect_1,d9_rlvect_1,t38_rlvect_1,t203_xcmplx_1,t6_xcmplx_1,t6_xcmplx_1,d10_rlvect_1,t45_rlvect_1,l16_anproj_2,l16_anproj_2,d9_rlvect_1,d9_rlvect_1,d9_rlvect_1,d9_rlvect_1,d7_xcmplx_0,d9_rlvect_1,t6_xcmplx_1,t6_xcmplx_1]), [file(anproj_2,t6_anproj_2),interesting(0.38)]). fof(l25_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,k1_numbers) => ! [F] : ( m1_subset_1(F,k1_numbers) => ! [G] : ( m1_subset_1(G,k1_numbers) => k4_rlvect_1(A,k4_rlvect_1(A,k3_rlvect_1(A,B,0),k3_rlvect_1(A,C,k4_real_1(E,F))),k3_rlvect_1(A,D,k4_real_1(k1_real_1(E),G))) = k3_rlvect_1(A,k6_rlvect_1(A,k3_rlvect_1(A,C,F),k3_rlvect_1(A,D,G)),E) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t23_rlvect_1,t10_rlvect_1,d9_rlvect_1,d9_rlvect_1,l16_anproj_2,d9_rlvect_1,d11_rlvect_1]), [file(anproj_2,l25_anproj_2),interesting(0.38)]). fof(t5_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ( ! [F] : ( m1_subset_1(F,k1_numbers) => ! [G] : ( m1_subset_1(G,k1_numbers) => ! [H] : ( m1_subset_1(H,k1_numbers) => ! [I] : ( m1_subset_1(I,k1_numbers) => ( k4_rlvect_1(A,k4_rlvect_1(A,k4_rlvect_1(A,k3_rlvect_1(A,B,F),k3_rlvect_1(A,C,G)),k3_rlvect_1(A,D,H)),k3_rlvect_1(A,E,I)) = k1_rlvect_1(A) => ( F = 0 & G = 0 & H = 0 & I = 0 ) ) ) ) ) ) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ~ ( v8_rlvect_1(F,A) & r2_anproj_1(A,B,C,F) & r2_anproj_1(A,D,E,F) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t2_anproj_2,t2_anproj_2,t11_anproj_1,t11_anproj_1,t28_rlvect_1,d11_rlvect_1,t29_rlvect_1,d9_rlvect_1,d9_rlvect_1,d9_rlvect_1,d6_rlvect_1,t23_rlvect_1,t23_rlvect_1,t10_rlvect_1,d13_rlvect_1]), [file(anproj_2,t5_anproj_2),interesting(0.36)]). fof(t24_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & ~ v3_realset2(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(k6_anproj_1(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k6_anproj_1(A))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k6_anproj_1(A))) => ( r1_collsp(k6_anproj_1(A),B,C,D) <=> ? [E] : ( m1_subset_1(E,u1_struct_0(A)) & ? [F] : ( m1_subset_1(F,u1_struct_0(A)) & ? [G] : ( m1_subset_1(G,u1_struct_0(A)) & B = k3_anproj_1(A,E) & C = k3_anproj_1(A,F) & D = k3_anproj_1(A,G) & v8_rlvect_1(E,A) & v8_rlvect_1(F,A) & v8_rlvect_1(G,A) & r2_anproj_1(A,E,F,G) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_collsp,t40_anproj_1,t41_anproj_1,d2_collsp]), [file(anproj_2,t24_anproj_2),interesting(0.34)]). fof(t3_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( ( ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ? [F] : ( m1_subset_1(F,k1_numbers) & ? [G] : ( m1_subset_1(G,k1_numbers) & ? [H] : ( m1_subset_1(H,k1_numbers) & E = k4_rlvect_1(A,k4_rlvect_1(A,k3_rlvect_1(A,B,F),k3_rlvect_1(A,C,G)),k3_rlvect_1(A,D,H)) ) ) ) ) & ! [E] : ( m1_subset_1(E,k1_numbers) => ! [F] : ( m1_subset_1(F,k1_numbers) => ! [G] : ( m1_subset_1(G,k1_numbers) => ( k4_rlvect_1(A,k4_rlvect_1(A,k3_rlvect_1(A,B,E),k3_rlvect_1(A,C,F)),k3_rlvect_1(A,D,G)) = k1_rlvect_1(A) => ( E = 0 & F = 0 & G = 0 ) ) ) ) ) ) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ? [G] : ( m1_subset_1(G,u1_struct_0(A)) & r2_anproj_1(A,B,C,G) & r2_anproj_1(A,E,F,G) & v8_rlvect_1(G,A) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t1_anproj_2,l4_anproj_2,l4_anproj_2,l5_anproj_2,d9_rlvect_1,d9_rlvect_1,d9_rlvect_1,t16_anproj_1,t16_anproj_1,d13_rlvect_1,t16_anproj_1,t15_anproj_1,d13_rlvect_1,t16_anproj_1,t15_anproj_1,d9_rlvect_1,t23_rlvect_1,t10_rlvect_1,t23_rlvect_1,t10_rlvect_1,t11_anproj_1,t11_anproj_1,d9_rlvect_1,t23_rlvect_1,t10_rlvect_1,t23_rlvect_1,t10_rlvect_1,t11_anproj_1,t11_anproj_1,t203_xcmplx_1,t6_xcmplx_1,d13_rlvect_1,t38_rlvect_1,t39_rlvect_1,d10_rlvect_1,t31_rlvect_1,d2_anproj_1,d7_xcmplx_0,t23_rlvect_1,t10_rlvect_1,t11_anproj_1,t11_anproj_1]), [file(anproj_2,t3_anproj_2),interesting(0.33)]). fof(l90_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & ~ v3_realset2(A) & l2_rlvect_1(A) ) => ( ? [B] : ( m1_subset_1(B,u1_struct_0(A)) & ? [C] : ( m1_subset_1(C,u1_struct_0(A)) & ? [D] : ( m1_subset_1(D,u1_struct_0(A)) & ? [E] : ( m1_subset_1(E,u1_struct_0(A)) & ! [F] : ( m1_subset_1(F,k1_numbers) => ! [G] : ( m1_subset_1(G,k1_numbers) => ! [H] : ( m1_subset_1(H,k1_numbers) => ! [I] : ( m1_subset_1(I,k1_numbers) => ( k4_rlvect_1(A,k4_rlvect_1(A,k4_rlvect_1(A,k3_rlvect_1(A,B,F),k3_rlvect_1(A,C,G)),k3_rlvect_1(A,D,H)),k3_rlvect_1(A,E,I)) = k1_rlvect_1(A) => ( F = 0 & G = 0 & H = 0 & I = 0 ) ) ) ) ) ) ) ) ) ) => ( v4_collsp(k6_anproj_1(A)) & v3_anproj_2(k6_anproj_1(A)) ) ) ) ), inference(mizar_proof,[status(thm)],[l89_anproj_2,l72_anproj_2,l74_anproj_2]), [file(anproj_2,l90_anproj_2),interesting(0.32)]). fof(t1_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( ! [E] : ( m1_subset_1(E,k1_numbers) => ! [F] : ( m1_subset_1(F,k1_numbers) => ! [G] : ( m1_subset_1(G,k1_numbers) => ( k4_rlvect_1(A,k4_rlvect_1(A,k3_rlvect_1(A,B,E),k3_rlvect_1(A,C,F)),k3_rlvect_1(A,D,G)) = k1_rlvect_1(A) => ( E = 0 & F = 0 & G = 0 ) ) ) ) ) => ( v8_rlvect_1(B,A) & v8_rlvect_1(C,A) & v8_rlvect_1(D,A) & ~ r2_anproj_1(A,B,C,D) & ~ r1_anproj_1(A,B,C) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d13_rlvect_1,t10_rlvect_1,t10_rlvect_1,d9_rlvect_1,t23_rlvect_1,t23_rlvect_1,d13_rlvect_1,t10_rlvect_1,t10_rlvect_1,d9_rlvect_1,t23_rlvect_1,t23_rlvect_1,d13_rlvect_1,t10_rlvect_1,t10_rlvect_1,d9_rlvect_1,t23_rlvect_1,t23_rlvect_1,d3_anproj_1,t17_anproj_1]), [file(anproj_2,t1_anproj_2),interesting(0.31)]). fof(t34_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & ~ v3_realset2(A) & l2_rlvect_1(A) ) => ~ ( ? [B] : ( m1_subset_1(B,u1_struct_0(A)) & ? [C] : ( m1_subset_1(C,u1_struct_0(A)) & ? [D] : ( m1_subset_1(D,u1_struct_0(A)) & ? [E] : ( m1_subset_1(E,u1_struct_0(A)) & ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ? [G] : ( m1_subset_1(G,k1_numbers) & ? [H] : ( m1_subset_1(H,k1_numbers) & ? [I] : ( m1_subset_1(I,k1_numbers) & ? [J] : ( m1_subset_1(J,k1_numbers) & F = k4_rlvect_1(A,k4_rlvect_1(A,k4_rlvect_1(A,k3_rlvect_1(A,B,G),k3_rlvect_1(A,C,H)),k3_rlvect_1(A,D,I)),k3_rlvect_1(A,E,J)) ) ) ) ) ) & ! [F] : ( m1_subset_1(F,k1_numbers) => ! [G] : ( m1_subset_1(G,k1_numbers) => ! [H] : ( m1_subset_1(H,k1_numbers) => ! [I] : ( m1_subset_1(I,k1_numbers) => ( k4_rlvect_1(A,k4_rlvect_1(A,k4_rlvect_1(A,k3_rlvect_1(A,B,F),k3_rlvect_1(A,C,G)),k3_rlvect_1(A,D,H)),k3_rlvect_1(A,E,I)) = k1_rlvect_1(A) => ( F = 0 & G = 0 & H = 0 & I = 0 ) ) ) ) ) ) ) ) ) ) & ! [B] : ( ( ~ v3_struct_0(B) & v2_collsp(B) & v3_collsp(B) & v4_collsp(B) & v2_anproj_2(B) & v3_anproj_2(B) & l1_collsp(B) ) => ~ ( B = k6_anproj_1(A) & v8_anproj_2(B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l90_anproj_2,t32_anproj_2,t33_anproj_2]), [file(anproj_2,t34_anproj_2),interesting(0.30)]). fof(t2_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ( ! [F] : ( m1_subset_1(F,k1_numbers) => ! [G] : ( m1_subset_1(G,k1_numbers) => ! [H] : ( m1_subset_1(H,k1_numbers) => ! [I] : ( m1_subset_1(I,k1_numbers) => ( k4_rlvect_1(A,k4_rlvect_1(A,k4_rlvect_1(A,k3_rlvect_1(A,B,F),k3_rlvect_1(A,C,G)),k3_rlvect_1(A,D,H)),k3_rlvect_1(A,E,I)) = k1_rlvect_1(A) => ( F = 0 & G = 0 & H = 0 & I = 0 ) ) ) ) ) ) => ( v8_rlvect_1(B,A) & v8_rlvect_1(C,A) & ~ r1_anproj_1(A,B,C) & v8_rlvect_1(D,A) & v8_rlvect_1(E,A) & ~ r1_anproj_1(A,D,E) & ~ r2_anproj_1(A,B,C,D) & ~ r2_anproj_1(A,D,E,B) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d6_rlvect_1,t10_rlvect_1,t23_rlvect_1,t10_rlvect_1,t23_rlvect_1,t1_anproj_2]), [file(anproj_2,t2_anproj_2),interesting(0.27)]). fof(t29_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & ~ v3_realset2(A) & l2_rlvect_1(A) ) => ~ ( ? [B] : ( m1_subset_1(B,u1_struct_0(A)) & ? [C] : ( m1_subset_1(C,u1_struct_0(A)) & ? [D] : ( m1_subset_1(D,u1_struct_0(A)) & ! [E] : ( m1_subset_1(E,k1_numbers) => ! [F] : ( m1_subset_1(F,k1_numbers) => ! [G] : ( m1_subset_1(G,k1_numbers) => ( k4_rlvect_1(A,k4_rlvect_1(A,k3_rlvect_1(A,B,E),k3_rlvect_1(A,C,F)),k3_rlvect_1(A,D,G)) = k1_rlvect_1(A) => ( E = 0 & F = 0 & G = 0 ) ) ) ) ) & ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ? [F] : ( m1_subset_1(F,k1_numbers) & ? [G] : ( m1_subset_1(G,k1_numbers) & ? [H] : ( m1_subset_1(H,k1_numbers) & E = k4_rlvect_1(A,k4_rlvect_1(A,k3_rlvect_1(A,B,F),k3_rlvect_1(A,C,G)),k3_rlvect_1(A,D,H)) ) ) ) ) ) ) ) & ! [B] : ( m1_subset_1(B,u1_struct_0(k6_anproj_1(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k6_anproj_1(A))) => ~ ( B != C & ! [D] : ( m1_subset_1(D,u1_struct_0(k6_anproj_1(A))) => ! [E] : ( m1_subset_1(E,u1_struct_0(k6_anproj_1(A))) => ? [F] : ( m1_subset_1(F,u1_struct_0(k6_anproj_1(A))) & r1_collsp(k6_anproj_1(A),B,C,F) & r1_collsp(k6_anproj_1(A),D,E,F) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t1_anproj_2,t42_anproj_1,t1_anproj_2,t35_anproj_1,t42_anproj_1,t42_anproj_1,t3_anproj_2,t42_anproj_1,t24_anproj_2,t24_anproj_2]), [file(anproj_2,t29_anproj_2),interesting(0.25)]). fof(t4_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ( ( ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ? [G] : ( m1_subset_1(G,k1_numbers) & ? [H] : ( m1_subset_1(H,k1_numbers) & ? [I] : ( m1_subset_1(I,k1_numbers) & ? [J] : ( m1_subset_1(J,k1_numbers) & F = k4_rlvect_1(A,k4_rlvect_1(A,k4_rlvect_1(A,k3_rlvect_1(A,B,G),k3_rlvect_1(A,C,H)),k3_rlvect_1(A,D,I)),k3_rlvect_1(A,E,J)) ) ) ) ) ) & ! [F] : ( m1_subset_1(F,k1_numbers) => ! [G] : ( m1_subset_1(G,k1_numbers) => ! [H] : ( m1_subset_1(H,k1_numbers) => ! [I] : ( m1_subset_1(I,k1_numbers) => ( k4_rlvect_1(A,k4_rlvect_1(A,k4_rlvect_1(A,k3_rlvect_1(A,B,F),k3_rlvect_1(A,C,G)),k3_rlvect_1(A,D,H)),k3_rlvect_1(A,E,I)) = k1_rlvect_1(A) => ( F = 0 & G = 0 & H = 0 & I = 0 ) ) ) ) ) ) ) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ~ ( v8_rlvect_1(F,A) & v8_rlvect_1(G,A) & ! [H] : ( m1_subset_1(H,u1_struct_0(A)) => ! [I] : ( m1_subset_1(I,u1_struct_0(A)) => ~ ( r2_anproj_1(A,F,G,I) & r2_anproj_1(A,C,D,H) & r2_anproj_1(A,B,I,H) & v8_rlvect_1(H,A) & v8_rlvect_1(I,A) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t2_anproj_2,l7_anproj_2,l7_anproj_2,l8_anproj_2,d9_rlvect_1,d9_rlvect_1,d9_rlvect_1,d9_rlvect_1,t16_anproj_1,t16_anproj_1,t16_anproj_1,t16_anproj_1,t23_rlvect_1,t10_rlvect_1,t16_anproj_1,t23_rlvect_1,t10_rlvect_1,d7_xcmplx_0,t23_rlvect_1,t10_rlvect_1,t11_anproj_1,t10_rlvect_1,t23_rlvect_1,d7_xcmplx_0,t6_xcmplx_1,t203_xcmplx_1,l7_anproj_2,t5_anproj_1,d13_rlvect_1,t16_anproj_1,t23_rlvect_1,t23_rlvect_1,t10_rlvect_1,t10_rlvect_1,t23_rlvect_1,d13_rlvect_1,t5_anproj_1,l10_anproj_2,t23_rlvect_1,t10_rlvect_1,d13_rlvect_1,t10_rlvect_1,t23_rlvect_1,t10_rlvect_1,t23_rlvect_1,t11_anproj_1]), [file(anproj_2,t4_anproj_2),interesting(0.25)]). fof(l39_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,k1_numbers) => ! [G] : ( m1_subset_1(G,k1_numbers) => ! [H] : ( m1_subset_1(H,k1_numbers) => ! [I] : ( m1_subset_1(I,k1_numbers) => ! [J] : ( m1_subset_1(J,k1_numbers) => ! [K] : ( m1_subset_1(K,k1_numbers) => ( ( J = k4_real_1(k4_real_1(k5_real_1(k4_real_1(F,G),k4_real_1(F,H)),k2_real_1(k5_real_1(k4_real_1(F,H),k4_real_1(I,H)))),K) & B = k4_rlvect_1(A,k4_rlvect_1(A,k3_rlvect_1(A,C,k3_real_1(J,K)),k3_rlvect_1(A,D,k4_real_1(J,I))),k3_rlvect_1(A,E,k4_real_1(K,G))) ) => ( H = 0 | I = F | B = k3_rlvect_1(A,k4_rlvect_1(A,k4_rlvect_1(A,k3_rlvect_1(A,C,k5_real_1(k4_real_1(F,G),k4_real_1(I,H))),k3_rlvect_1(A,D,k4_real_1(k4_real_1(I,F),k5_real_1(G,H)))),k3_rlvect_1(A,E,k4_real_1(k4_real_1(H,G),k5_real_1(F,I)))),k4_real_1(K,k2_real_1(k5_real_1(k4_real_1(F,H),k4_real_1(I,H))))) ) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l36_anproj_2,d7_xcmplx_0,d9_rlvect_1,d9_rlvect_1,d7_xcmplx_0,d9_rlvect_1,d9_rlvect_1,d9_rlvect_1]), [file(anproj_2,l39_anproj_2),interesting(0.18)]). fof(t32_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & ~ v3_realset2(A) & l2_rlvect_1(A) ) => ~ ( ? [B] : ( m1_subset_1(B,u1_struct_0(A)) & ? [C] : ( m1_subset_1(C,u1_struct_0(A)) & ? [D] : ( m1_subset_1(D,u1_struct_0(A)) & ? [E] : ( m1_subset_1(E,u1_struct_0(A)) & ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ? [G] : ( m1_subset_1(G,k1_numbers) & ? [H] : ( m1_subset_1(H,k1_numbers) & ? [I] : ( m1_subset_1(I,k1_numbers) & ? [J] : ( m1_subset_1(J,k1_numbers) & F = k4_rlvect_1(A,k4_rlvect_1(A,k4_rlvect_1(A,k3_rlvect_1(A,B,G),k3_rlvect_1(A,C,H)),k3_rlvect_1(A,D,I)),k3_rlvect_1(A,E,J)) ) ) ) ) ) & ! [F] : ( m1_subset_1(F,k1_numbers) => ! [G] : ( m1_subset_1(G,k1_numbers) => ! [H] : ( m1_subset_1(H,k1_numbers) => ! [I] : ( m1_subset_1(I,k1_numbers) => ( k4_rlvect_1(A,k4_rlvect_1(A,k4_rlvect_1(A,k3_rlvect_1(A,B,F),k3_rlvect_1(A,C,G)),k3_rlvect_1(A,D,H)),k3_rlvect_1(A,E,I)) = k1_rlvect_1(A) => ( F = 0 & G = 0 & H = 0 & I = 0 ) ) ) ) ) ) ) ) ) ) & ! [B] : ( m1_subset_1(B,u1_struct_0(k6_anproj_1(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k6_anproj_1(A))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k6_anproj_1(A))) => ~ ( ~ r1_collsp(k6_anproj_1(A),B,C,D) & ! [E] : ( m1_subset_1(E,u1_struct_0(k6_anproj_1(A))) => ! [F] : ( m1_subset_1(F,u1_struct_0(k6_anproj_1(A))) => ? [G] : ( m1_subset_1(G,u1_struct_0(k6_anproj_1(A))) & ? [H] : ( m1_subset_1(H,u1_struct_0(k6_anproj_1(A))) & r1_collsp(k6_anproj_1(A),E,F,H) & r1_collsp(k6_anproj_1(A),C,D,G) & r1_collsp(k6_anproj_1(A),B,H,G) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t2_anproj_2,t42_anproj_1,d2_collsp,t41_anproj_1,t42_anproj_1,t42_anproj_1,t4_anproj_2,t42_anproj_1,t24_anproj_2,t24_anproj_2,t24_anproj_2]), [file(anproj_2,t32_anproj_2),interesting(0.16)]). fof(l41_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ! [H] : ( m1_subset_1(H,k1_numbers) => ! [I] : ( m1_subset_1(I,k1_numbers) => ! [J] : ( m1_subset_1(J,k1_numbers) => ! [K] : ( m1_subset_1(K,k1_numbers) => ! [L] : ( m1_subset_1(L,k1_numbers) => ! [M] : ( m1_subset_1(M,k1_numbers) => ( ( B = k4_rlvect_1(A,k4_rlvect_1(A,k3_rlvect_1(A,C,k5_real_1(k4_real_1(H,I),k4_real_1(J,K))),k3_rlvect_1(A,D,k4_real_1(k4_real_1(J,H),k5_real_1(I,K)))),k3_rlvect_1(A,E,k4_real_1(k4_real_1(K,I),k5_real_1(H,J)))) & F = k4_rlvect_1(A,k4_rlvect_1(A,C,k3_rlvect_1(A,D,H)),k3_rlvect_1(A,E,I)) & G = k4_rlvect_1(A,k4_rlvect_1(A,C,k3_rlvect_1(A,D,J)),k3_rlvect_1(A,E,K)) & k3_real_1(L,M) = k5_real_1(k4_real_1(J,K),k4_real_1(H,I)) & k3_real_1(k4_real_1(L,H),k4_real_1(M,J)) = k4_real_1(k4_real_1(J,H),k5_real_1(K,I)) & k3_real_1(k4_real_1(L,I),k4_real_1(M,K)) = k4_real_1(k4_real_1(K,I),k5_real_1(J,H)) ) => k4_rlvect_1(A,k4_rlvect_1(A,k3_rlvect_1(A,B,1),k3_rlvect_1(A,F,L)),k3_rlvect_1(A,G,M)) = k1_rlvect_1(A) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_rlvect_1,d6_rlvect_1,d9_rlvect_1,d9_rlvect_1,d9_rlvect_1,d9_rlvect_1,l40_anproj_2,d9_rlvect_1,d9_rlvect_1,d9_rlvect_1,d9_rlvect_1,d9_rlvect_1,d9_rlvect_1,d9_rlvect_1,l40_anproj_2,d9_rlvect_1,d9_rlvect_1,d9_rlvect_1,t23_rlvect_1,t10_rlvect_1,t23_rlvect_1,t23_rlvect_1,t10_rlvect_1]), [file(anproj_2,l41_anproj_2),interesting(0.13)]). fof(t35_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & ~ v3_realset2(A) & l2_rlvect_1(A) ) => ~ ( ? [B] : ( m1_subset_1(B,u1_struct_0(A)) & ? [C] : ( m1_subset_1(C,u1_struct_0(A)) & ? [D] : ( m1_subset_1(D,u1_struct_0(A)) & ? [E] : ( m1_subset_1(E,u1_struct_0(A)) & ! [F] : ( m1_subset_1(F,k1_numbers) => ! [G] : ( m1_subset_1(G,k1_numbers) => ! [H] : ( m1_subset_1(H,k1_numbers) => ! [I] : ( m1_subset_1(I,k1_numbers) => ( k4_rlvect_1(A,k4_rlvect_1(A,k4_rlvect_1(A,k3_rlvect_1(A,B,F),k3_rlvect_1(A,C,G)),k3_rlvect_1(A,D,H)),k3_rlvect_1(A,E,I)) = k1_rlvect_1(A) => ( F = 0 & G = 0 & H = 0 & I = 0 ) ) ) ) ) ) ) ) ) ) & ! [B] : ( ( ~ v3_struct_0(B) & v2_collsp(B) & v3_collsp(B) & v4_collsp(B) & v2_anproj_2(B) & v3_anproj_2(B) & l1_collsp(B) ) => ~ ( B = k6_anproj_1(A) & ~ v7_anproj_2(B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t2_anproj_2,l89_anproj_2,l75_anproj_2,t42_anproj_1,d14_anproj_2,d2_collsp,t42_anproj_1,t41_anproj_1,t5_anproj_2]), [file(anproj_2,t35_anproj_2),interesting(0.10)]). fof(t36_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & ~ v3_realset2(A) & l2_rlvect_1(A) ) => ~ ( ? [B] : ( m1_subset_1(B,u1_struct_0(A)) & ? [C] : ( m1_subset_1(C,u1_struct_0(A)) & ? [D] : ( m1_subset_1(D,u1_struct_0(A)) & ? [E] : ( m1_subset_1(E,u1_struct_0(A)) & ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ? [G] : ( m1_subset_1(G,k1_numbers) & ? [H] : ( m1_subset_1(H,k1_numbers) & ? [I] : ( m1_subset_1(I,k1_numbers) & ? [J] : ( m1_subset_1(J,k1_numbers) & F = k4_rlvect_1(A,k4_rlvect_1(A,k4_rlvect_1(A,k3_rlvect_1(A,B,G),k3_rlvect_1(A,C,H)),k3_rlvect_1(A,D,I)),k3_rlvect_1(A,E,J)) ) ) ) ) ) & ! [F] : ( m1_subset_1(F,k1_numbers) => ! [G] : ( m1_subset_1(G,k1_numbers) => ! [H] : ( m1_subset_1(H,k1_numbers) => ! [I] : ( m1_subset_1(I,k1_numbers) => ( k4_rlvect_1(A,k4_rlvect_1(A,k4_rlvect_1(A,k3_rlvect_1(A,B,F),k3_rlvect_1(A,C,G)),k3_rlvect_1(A,D,H)),k3_rlvect_1(A,E,I)) = k1_rlvect_1(A) => ( F = 0 & G = 0 & H = 0 & I = 0 ) ) ) ) ) ) ) ) ) ) & ! [B] : ( ( ~ v3_struct_0(B) & v2_collsp(B) & v3_collsp(B) & v4_collsp(B) & v2_anproj_2(B) & v3_anproj_2(B) & l1_collsp(B) ) => ~ ( B = k6_anproj_1(A) & ~ v7_anproj_2(B) & v8_anproj_2(B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t35_anproj_2,t34_anproj_2]), [file(anproj_2,t36_anproj_2),interesting(0.08)]). fof(d7_anproj_2,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_collsp(A) ) => ( v2_collsp(A) <=> ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( r1_collsp(A,B,C,B) & r1_collsp(A,B,B,C) & r1_collsp(A,B,C,C) ) ) ) ) ) ) ), file(anproj_2,d7_anproj_2), [interesting(0.00)]). fof(t42_anproj_1,theorem,( ! [A,B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v7_rlvect_1(B) & ~ v3_realset2(B) & l2_rlvect_1(B) ) => ( m1_subset_1(A,u1_struct_0(k6_anproj_1(B))) <=> ? [C] : ( m1_subset_1(C,u1_struct_0(B)) & v8_rlvect_1(C,B) & A = k3_anproj_1(B,C) ) ) ) ), file(anproj_1,t42_anproj_1), [interesting(0.00)]). fof(t16_anproj_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( ~ ( ~ r1_anproj_1(A,B,C) & ~ r1_anproj_1(A,D,B) & ~ r1_anproj_1(A,C,D) ) => r2_anproj_1(A,D,B,C) ) ) ) ) ) ), file(anproj_1,t16_anproj_1), [interesting(0.00)]). fof(d2_collsp,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_collsp(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( r1_collsp(A,B,C,D) <=> r2_hidden(k4_domain_1(u1_struct_0(A),u1_struct_0(A),u1_struct_0(A),B,C,D),u1_collsp(A)) ) ) ) ) ) ), file(collsp,d2_collsp), [interesting(0.00)]). fof(t40_anproj_1,theorem,( ! [A,B,C,D] : ( ( ~ v3_struct_0(D) & v3_rlvect_1(D) & v4_rlvect_1(D) & v5_rlvect_1(D) & v6_rlvect_1(D) & v7_rlvect_1(D) & ~ v3_realset2(D) & l2_rlvect_1(D) ) => ~ ( r2_hidden(k3_mcart_1(A,B,C),u1_collsp(k6_anproj_1(D))) & ! [E] : ( m1_subset_1(E,u1_struct_0(D)) => ! [F] : ( m1_subset_1(F,u1_struct_0(D)) => ! [G] : ( m1_subset_1(G,u1_struct_0(D)) => ~ ( A = k3_anproj_1(D,E) & B = k3_anproj_1(D,F) & C = k3_anproj_1(D,G) & v8_rlvect_1(E,D) & v8_rlvect_1(F,D) & v8_rlvect_1(G,D) & r2_anproj_1(D,E,F,G) ) ) ) ) ) ) ), file(anproj_1,t40_anproj_1), [interesting(0.00)]). fof(t41_anproj_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & ~ v3_realset2(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( ( v8_rlvect_1(B,A) & v8_rlvect_1(C,A) & v8_rlvect_1(D,A) ) => ( r2_hidden(k3_mcart_1(k3_anproj_1(A,B),k3_anproj_1(A,C),k3_anproj_1(A,D)),u1_collsp(k6_anproj_1(A))) <=> r2_anproj_1(A,B,C,D) ) ) ) ) ) ) ), file(anproj_1,t41_anproj_1), [interesting(0.00)]). fof(d8_anproj_2,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_collsp(A) ) => ( v3_collsp(A) <=> ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ( ( r1_collsp(A,B,C,D) & r1_collsp(A,B,C,E) & r1_collsp(A,B,C,F) ) => ( B = C | r1_collsp(A,D,E,F) ) ) ) ) ) ) ) ) ) ), file(anproj_2,d8_anproj_2), [interesting(0.00)]). fof(t35_anproj_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & ~ v3_realset2(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( ( v8_rlvect_1(B,A) & v8_rlvect_1(C,A) ) => ( k3_anproj_1(A,B) = k3_anproj_1(A,C) <=> r1_anproj_1(A,B,C) ) ) ) ) ) ), file(anproj_1,t35_anproj_1), [interesting(0.00)]). fof(t9_anproj_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ( ( r1_anproj_1(A,B,C) & r1_anproj_1(A,D,E) & r1_anproj_1(A,F,G) & r2_anproj_1(A,B,D,F) ) => r2_anproj_1(A,C,E,G) ) ) ) ) ) ) ) ) ), file(anproj_1,t9_anproj_1), [interesting(0.00)]). fof(t19_anproj_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ( ( r2_anproj_1(A,B,C,D) & r2_anproj_1(A,B,C,E) & r2_anproj_1(A,B,C,F) & v8_rlvect_1(B,A) & v8_rlvect_1(C,A) ) => ( r1_anproj_1(A,B,C) | r2_anproj_1(A,D,E,F) ) ) ) ) ) ) ) ) ), file(anproj_1,t19_anproj_1), [interesting(0.00)]). fof(d9_anproj_2,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_collsp(A) ) => ( v2_anproj_2(A) <=> ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ~ ( r1_collsp(A,B,C,E) & r1_collsp(A,C,D,F) & ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ~ ( r1_collsp(A,B,D,G) & r1_collsp(A,E,F,G) ) ) ) ) ) ) ) ) ) ) ), file(anproj_2,d9_anproj_2), [interesting(0.00)]). fof(t10_anproj_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( r2_anproj_1(A,B,C,D) => ( r2_anproj_1(A,B,D,C) & r2_anproj_1(A,C,B,D) & r2_anproj_1(A,D,C,B) & r2_anproj_1(A,D,B,C) & r2_anproj_1(A,C,D,B) ) ) ) ) ) ) ), file(anproj_1,t10_anproj_1), [interesting(0.00)]). fof(t25_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & ~ v3_realset2(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(k6_anproj_1(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k6_anproj_1(A))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k6_anproj_1(A))) => ( r1_collsp(k6_anproj_1(A),B,C,D) => ( r1_collsp(k6_anproj_1(A),B,D,C) & r1_collsp(k6_anproj_1(A),C,B,D) & r1_collsp(k6_anproj_1(A),D,C,B) & r1_collsp(k6_anproj_1(A),D,B,C) & r1_collsp(k6_anproj_1(A),C,D,B) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t24_anproj_2,t10_anproj_1,t24_anproj_2]), [file(anproj_2,t25_anproj_2),interesting(0.00)]). fof(l69_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & ~ v3_realset2(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(k6_anproj_1(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k6_anproj_1(A))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k6_anproj_1(A))) => ! [E] : ( m1_subset_1(E,u1_struct_0(k6_anproj_1(A))) => ! [F] : ( m1_subset_1(F,u1_struct_0(k6_anproj_1(A))) => ~ ( r1_collsp(k6_anproj_1(A),B,C,D) & r1_collsp(k6_anproj_1(A),B,C,E) & r1_collsp(k6_anproj_1(A),C,D,F) & ! [G] : ( m1_subset_1(G,u1_struct_0(k6_anproj_1(A))) => ~ ( r1_collsp(k6_anproj_1(A),B,D,G) & r1_collsp(k6_anproj_1(A),E,F,G) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d7_anproj_2,d7_anproj_2,d7_anproj_2,d8_anproj_2,d7_anproj_2,d7_anproj_2,t25_anproj_2,d8_anproj_2,d7_anproj_2]), [file(anproj_2,l69_anproj_2),interesting(0.00)]). fof(t20_anproj_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ~ ( ~ r2_anproj_1(A,B,C,D) & r2_anproj_1(A,B,C,E) & r2_anproj_1(A,C,D,F) & ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ~ ( r2_anproj_1(A,B,D,G) & r2_anproj_1(A,E,F,G) & v8_rlvect_1(G,A) ) ) ) ) ) ) ) ) ) ), file(anproj_1,t20_anproj_1), [interesting(0.00)]). fof(l70_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & ~ v3_realset2(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(k6_anproj_1(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k6_anproj_1(A))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k6_anproj_1(A))) => ! [E] : ( m1_subset_1(E,u1_struct_0(k6_anproj_1(A))) => ! [F] : ( m1_subset_1(F,u1_struct_0(k6_anproj_1(A))) => ~ ( ~ r1_collsp(k6_anproj_1(A),B,C,D) & r1_collsp(k6_anproj_1(A),B,C,E) & r1_collsp(k6_anproj_1(A),C,D,F) & ! [G] : ( m1_subset_1(G,u1_struct_0(k6_anproj_1(A))) => ~ ( r1_collsp(k6_anproj_1(A),B,D,G) & r1_collsp(k6_anproj_1(A),E,F,G) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t24_anproj_2,t24_anproj_2,t35_anproj_1,t9_anproj_1,t24_anproj_2,t20_anproj_1,t42_anproj_1,t24_anproj_2]), [file(anproj_2,l70_anproj_2),interesting(0.00)]). fof(t23_anproj_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ! [H] : ( m1_subset_1(H,u1_struct_0(A)) => ~ ( r2_anproj_1(A,B,C,D) & r2_anproj_1(A,E,F,D) & r2_anproj_1(A,B,E,G) & r2_anproj_1(A,C,F,G) & r2_anproj_1(A,B,F,H) & r2_anproj_1(A,C,E,H) & r2_anproj_1(A,G,D,H) & v8_rlvect_1(G,A) & v8_rlvect_1(D,A) & v8_rlvect_1(H,A) & ~ r2_anproj_1(A,B,C,F) & ~ r2_anproj_1(A,B,C,E) & ~ r2_anproj_1(A,B,E,F) & ~ r2_anproj_1(A,C,E,F) ) ) ) ) ) ) ) ) ) ), file(anproj_1,t23_anproj_1), [interesting(0.00)]). fof(t28_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & ~ v3_realset2(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(k6_anproj_1(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k6_anproj_1(A))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k6_anproj_1(A))) => ! [E] : ( m1_subset_1(E,u1_struct_0(k6_anproj_1(A))) => ! [F] : ( m1_subset_1(F,u1_struct_0(k6_anproj_1(A))) => ! [G] : ( m1_subset_1(G,u1_struct_0(k6_anproj_1(A))) => ! [H] : ( m1_subset_1(H,u1_struct_0(k6_anproj_1(A))) => ~ ( r1_collsp(k6_anproj_1(A),B,C,D) & r1_collsp(k6_anproj_1(A),E,F,D) & r1_collsp(k6_anproj_1(A),B,E,G) & r1_collsp(k6_anproj_1(A),C,F,G) & r1_collsp(k6_anproj_1(A),B,F,H) & r1_collsp(k6_anproj_1(A),C,E,H) & r1_collsp(k6_anproj_1(A),G,D,H) & ~ r1_collsp(k6_anproj_1(A),B,C,F) & ~ r1_collsp(k6_anproj_1(A),B,C,E) & ~ r1_collsp(k6_anproj_1(A),B,E,F) & ~ r1_collsp(k6_anproj_1(A),C,E,F) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t24_anproj_2,t24_anproj_2,t24_anproj_2,t24_anproj_2,t24_anproj_2,t24_anproj_2,t24_anproj_2,t35_anproj_1,t35_anproj_1,t35_anproj_1,t35_anproj_1,t35_anproj_1,t35_anproj_1,t35_anproj_1,t9_anproj_1,t9_anproj_1,t9_anproj_1,t9_anproj_1,t9_anproj_1,t9_anproj_1,t23_anproj_1,t24_anproj_2]), [file(anproj_2,t28_anproj_2),interesting(0.00)]). fof(d11_anproj_2,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v2_collsp(A) & v3_collsp(A) & v4_collsp(A) & v2_anproj_2(A) & v3_anproj_2(A) & l1_collsp(A) ) => ( v4_anproj_2(A) <=> ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ! [H] : ( m1_subset_1(H,u1_struct_0(A)) => ~ ( r1_collsp(A,B,C,D) & r1_collsp(A,E,F,D) & r1_collsp(A,B,E,G) & r1_collsp(A,C,F,G) & r1_collsp(A,B,F,H) & r1_collsp(A,C,E,H) & r1_collsp(A,G,D,H) & ~ r1_collsp(A,B,C,F) & ~ r1_collsp(A,B,C,E) & ~ r1_collsp(A,B,E,F) & ~ r1_collsp(A,C,E,F) ) ) ) ) ) ) ) ) ) ) ), file(anproj_2,d11_anproj_2), [interesting(0.00)]). fof(d12_anproj_2,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v2_collsp(A) & v3_collsp(A) & v4_collsp(A) & v2_anproj_2(A) & v3_anproj_2(A) & l1_collsp(A) ) => ( v5_anproj_2(A) <=> ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ! [H] : ( m1_subset_1(H,u1_struct_0(A)) => ! [I] : ( m1_subset_1(I,u1_struct_0(A)) => ! [J] : ( m1_subset_1(J,u1_struct_0(A)) => ! [K] : ( m1_subset_1(K,u1_struct_0(A)) => ( ( r1_collsp(A,C,D,K) & r1_collsp(A,F,G,K) & r1_collsp(A,D,E,I) & r1_collsp(A,G,H,I) & r1_collsp(A,C,E,J) & r1_collsp(A,F,H,J) & r1_collsp(A,B,C,F) & r1_collsp(A,B,D,G) & r1_collsp(A,B,E,H) ) => ( B = F | C = F | B = G | D = G | B = H | E = H | r1_collsp(A,B,C,D) | r1_collsp(A,B,C,E) | r1_collsp(A,B,D,E) | r1_collsp(A,I,J,K) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ), file(anproj_2,d12_anproj_2), [interesting(0.00)]). fof(d1_anproj_2,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( r1_anproj_2(A,B,C,D) <=> ( v8_rlvect_1(B,A) & v8_rlvect_1(C,A) & v8_rlvect_1(D,A) ) ) ) ) ) ) ), file(anproj_2,d1_anproj_2), [interesting(0.00)]). fof(d3_anproj_2,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ! [H] : ( m1_subset_1(H,u1_struct_0(A)) => ( r3_anproj_2(A,B,C,D,E,F,G,H) <=> ( r2_anproj_1(A,B,C,F) & r2_anproj_1(A,B,D,G) & r2_anproj_1(A,B,E,H) ) ) ) ) ) ) ) ) ) ) ), file(anproj_2,d3_anproj_2), [interesting(0.00)]). fof(d2_anproj_2,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ( r2_anproj_2(A,B,C,D,E,F,G) <=> ( r2_anproj_1(A,B,C,G) & r2_anproj_1(A,B,D,F) & r2_anproj_1(A,C,D,E) ) ) ) ) ) ) ) ) ) ), file(anproj_2,d2_anproj_2), [interesting(0.00)]). fof(d3_anproj_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( r2_anproj_1(A,B,C,D) <=> ? [E] : ( m1_subset_1(E,k1_numbers) & ? [F] : ( m1_subset_1(F,k1_numbers) & ? [G] : ( m1_subset_1(G,k1_numbers) & k4_rlvect_1(A,k4_rlvect_1(A,k3_rlvect_1(A,B,E),k3_rlvect_1(A,C,F)),k3_rlvect_1(A,D,G)) = k1_rlvect_1(A) & ~ ( E = 0 & F = 0 & G = 0 ) ) ) ) ) ) ) ) ) ), file(anproj_1,d3_anproj_1), [interesting(0.00)]). fof(d13_rlvect_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l2_struct_0(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ( v8_rlvect_1(B,A) <=> B != k1_rlvect_1(A) ) ) ) ), file(rlvect_1,d13_rlvect_1), [interesting(0.00)]). fof(t23_rlvect_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v7_rlvect_1(B) & l2_rlvect_1(B) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(B)) => ( ( A = 0 | C = k1_rlvect_1(B) ) => k3_rlvect_1(B,C,A) = k1_rlvect_1(B) ) ) ) ) ), file(rlvect_1,t23_rlvect_1), [interesting(0.00)]). fof(t10_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ( k2_rlvect_1(A,B,k1_rlvect_1(A)) = B & k2_rlvect_1(A,k1_rlvect_1(A),B) = B ) ) ) ), file(rlvect_1,t10_rlvect_1), [interesting(0.00)]). fof(t24_rlvect_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v7_rlvect_1(B) & l2_rlvect_1(B) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(B)) => ~ ( k3_rlvect_1(B,C,A) = k1_rlvect_1(B) & A != 0 & C != k1_rlvect_1(B) ) ) ) ) ), file(rlvect_1,t24_rlvect_1), [interesting(0.00)]). fof(t19_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( k2_rlvect_1(A,B,C) = k1_rlvect_1(A) => B = k5_rlvect_1(A,C) ) ) ) ) ), file(rlvect_1,t19_rlvect_1), [interesting(0.00)]). fof(t39_rlvect_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v7_rlvect_1(B) & l2_rlvect_1(B) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(B)) => k3_rlvect_1(B,k5_rlvect_1(B,C),A) = k5_rlvect_1(B,k3_rlvect_1(B,C,A)) ) ) ) ), file(rlvect_1,t39_rlvect_1), [interesting(0.00)]). fof(t38_rlvect_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v7_rlvect_1(B) & l2_rlvect_1(B) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(B)) => k3_rlvect_1(B,k5_rlvect_1(B,C),A) = k3_rlvect_1(B,C,k1_real_1(A)) ) ) ) ), file(rlvect_1,t38_rlvect_1), [interesting(0.00)]). fof(d2_anproj_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( r1_anproj_1(A,B,C) <=> ? [D] : ( m1_subset_1(D,k1_numbers) & ? [E] : ( m1_subset_1(E,k1_numbers) & k3_rlvect_1(A,B,D) = k3_rlvect_1(A,C,E) & D != 0 & E != 0 ) ) ) ) ) ) ), file(anproj_1,d2_anproj_1), [interesting(0.00)]). fof(d9_rlvect_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l2_rlvect_1(A) ) => ( v7_rlvect_1(A) <=> ( ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => k3_rlvect_1(A,k2_rlvect_1(A,C,D),B) = k2_rlvect_1(A,k3_rlvect_1(A,C,B),k3_rlvect_1(A,D,B)) ) ) ) & ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,k1_numbers) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => k3_rlvect_1(A,D,k3_real_1(B,C)) = k2_rlvect_1(A,k3_rlvect_1(A,D,B),k3_rlvect_1(A,D,C)) ) ) ) & ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,k1_numbers) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => k3_rlvect_1(A,D,k4_real_1(B,C)) = k3_rlvect_1(A,k3_rlvect_1(A,D,C),B) ) ) ) & ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k3_rlvect_1(A,B,1) = B ) ) ) ) ), file(rlvect_1,d9_rlvect_1), [interesting(0.00)]). fof(d7_xcmplx_0,definition,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ( ( A != 0 => ( B = k5_xcmplx_0(A) <=> k3_xcmplx_0(A,B) = 1 ) ) & ( A = 0 => ( B = k5_xcmplx_0(A) <=> B = 0 ) ) ) ) ) ), file(xcmplx_0,d7_xcmplx_0), [interesting(0.00)]). fof(t203_xcmplx_1,theorem,( k5_xcmplx_0(0) = 0 ), file(xcmplx_1,t203_xcmplx_1), [interesting(0.00)]). fof(t6_xcmplx_1,theorem,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ~ ( k3_xcmplx_0(A,B) = 0 & A != 0 & B != 0 ) ) ) ), file(xcmplx_1,t6_xcmplx_1), [interesting(0.00)]). fof(d10_rlvect_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ( ( v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( C = k5_rlvect_1(A,B) <=> k2_rlvect_1(A,B,C) = k1_rlvect_1(A) ) ) ) ) ) ), file(rlvect_1,d10_rlvect_1), [interesting(0.00)]). fof(t45_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => k5_rlvect_1(A,k2_rlvect_1(A,B,C)) = k2_rlvect_1(A,k5_rlvect_1(A,C),k5_rlvect_1(A,B)) ) ) ) ), file(rlvect_1,t45_rlvect_1), [interesting(0.00)]). fof(l16_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,k1_numbers) => k5_rlvect_1(A,k3_rlvect_1(A,B,C)) = k3_rlvect_1(A,B,k1_real_1(C)) ) ) ) ), inference(mizar_proof,[status(thm)],[t39_rlvect_1,t38_rlvect_1]), [file(anproj_2,l16_anproj_2),interesting(0.00)]). fof(t17_anproj_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( ~ r2_anproj_1(A,B,C,D) => ( v8_rlvect_1(B,A) & v8_rlvect_1(C,A) & v8_rlvect_1(D,A) & ~ r1_anproj_1(A,B,C) & ~ r1_anproj_1(A,C,D) & ~ r1_anproj_1(A,D,B) ) ) ) ) ) ) ), file(anproj_1,t17_anproj_1), [interesting(0.00)]). fof(l19_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,k1_numbers) => ( k3_rlvect_1(A,B,D) = C => ( D = 0 | r1_anproj_1(A,B,C) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_rlvect_1,d2_anproj_1]), [file(anproj_2,l19_anproj_2),interesting(0.00)]). fof(t5_anproj_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( r1_anproj_1(A,B,C) <=> ? [D] : ( m1_subset_1(D,k1_numbers) & D != 0 & B = k3_rlvect_1(A,C,D) ) ) ) ) ) ), file(anproj_1,t5_anproj_1), [interesting(0.00)]). fof(d6_rlvect_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_rlvect_1(A) ) => ( v4_rlvect_1(A) <=> ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => k2_rlvect_1(A,k2_rlvect_1(A,B,C),D) = k2_rlvect_1(A,B,k2_rlvect_1(A,C,D)) ) ) ) ) ) ), file(rlvect_1,d6_rlvect_1), [interesting(0.00)]). fof(t16_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ( k2_rlvect_1(A,B,k5_rlvect_1(A,B)) = k1_rlvect_1(A) & k2_rlvect_1(A,k5_rlvect_1(A,B),B) = k1_rlvect_1(A) ) ) ) ), file(rlvect_1,t16_rlvect_1), [interesting(0.00)]). fof(l20_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,k1_numbers) => ! [H] : ( m1_subset_1(H,k1_numbers) => ( ( B = k4_rlvect_1(A,C,k3_rlvect_1(A,D,G)) & E = k4_rlvect_1(A,C,k3_rlvect_1(A,F,H)) & r1_anproj_1(A,B,E) ) => ( G = 0 | r2_anproj_1(A,C,D,F) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t5_anproj_1,d9_rlvect_1,d9_rlvect_1,d6_rlvect_1,t16_rlvect_1,t10_rlvect_1,d6_rlvect_1,l16_anproj_2,d9_rlvect_1,d9_rlvect_1,t16_rlvect_1,l16_anproj_2,d3_anproj_1]), [file(anproj_2,l20_anproj_2),interesting(0.00)]). fof(l21_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,k1_numbers) => ( ( k3_rlvect_1(A,B,D) = C & v8_rlvect_1(B,A) ) => ( D = 0 | v8_rlvect_1(C,A) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d13_rlvect_1,t24_rlvect_1,d13_rlvect_1]), [file(anproj_2,l21_anproj_2),interesting(0.00)]). fof(l22_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ! [H] : ( m1_subset_1(H,k1_numbers) => ! [I] : ( m1_subset_1(I,k1_numbers) => ! [J] : ( m1_subset_1(J,k1_numbers) => ! [K] : ( m1_subset_1(K,k1_numbers) => ( ( B = k4_rlvect_1(A,k3_rlvect_1(A,C,J),k3_rlvect_1(A,D,K)) & C = k4_rlvect_1(A,E,k3_rlvect_1(A,F,H)) & D = k4_rlvect_1(A,E,k3_rlvect_1(A,G,I)) ) => B = k4_rlvect_1(A,k4_rlvect_1(A,k3_rlvect_1(A,E,k3_real_1(J,K)),k3_rlvect_1(A,F,k4_real_1(J,H))),k3_rlvect_1(A,G,k4_real_1(K,I))) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_rlvect_1,d9_rlvect_1,d9_rlvect_1,d9_rlvect_1,d6_rlvect_1,d6_rlvect_1,d9_rlvect_1]), [file(anproj_2,l22_anproj_2),interesting(0.00)]). fof(l23_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,k1_numbers) => ! [G] : ( m1_subset_1(G,k1_numbers) => ( B = k4_rlvect_1(A,k3_rlvect_1(A,C,F),k3_rlvect_1(A,D,G)) => B = k4_rlvect_1(A,k4_rlvect_1(A,k3_rlvect_1(A,E,0),k3_rlvect_1(A,C,F)),k3_rlvect_1(A,D,G)) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t10_rlvect_1,t23_rlvect_1]), [file(anproj_2,l23_anproj_2),interesting(0.00)]). fof(t13_anproj_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,k1_numbers) => ! [F] : ( m1_subset_1(F,k1_numbers) => ! [G] : ( m1_subset_1(G,k1_numbers) => ! [H] : ( m1_subset_1(H,k1_numbers) => ! [I] : ( m1_subset_1(I,k1_numbers) => ! [J] : ( m1_subset_1(J,k1_numbers) => ( k4_rlvect_1(A,k4_rlvect_1(A,k3_rlvect_1(A,B,E),k3_rlvect_1(A,C,F)),k3_rlvect_1(A,D,G)) = k4_rlvect_1(A,k4_rlvect_1(A,k3_rlvect_1(A,B,H),k3_rlvect_1(A,C,I)),k3_rlvect_1(A,D,J)) => ( r2_anproj_1(A,B,C,D) | ( E = H & F = I & G = J ) ) ) ) ) ) ) ) ) ) ) ) ) ), file(anproj_1,t13_anproj_1), [interesting(0.00)]). fof(l24_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => k4_rlvect_1(A,k3_rlvect_1(A,B,0),k3_rlvect_1(A,C,0)) = k1_rlvect_1(A) ) ) ) ), inference(mizar_proof,[status(thm)],[t23_rlvect_1,t10_rlvect_1,t23_rlvect_1]), [file(anproj_2,l24_anproj_2),interesting(0.00)]). fof(d11_rlvect_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => k6_rlvect_1(A,B,C) = k2_rlvect_1(A,B,k5_rlvect_1(A,C)) ) ) ) ), file(rlvect_1,d11_rlvect_1), [interesting(0.00)]). fof(t29_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k5_rlvect_1(A,B) = k3_rlvect_1(A,B,k1_real_1(1)) ) ) ), file(rlvect_1,t29_rlvect_1), [interesting(0.00)]). fof(t47_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => k5_rlvect_1(A,k6_rlvect_1(A,B,C)) = k2_rlvect_1(A,C,k5_rlvect_1(A,B)) ) ) ) ), file(rlvect_1,t47_rlvect_1), [interesting(0.00)]). fof(d13_anproj_2,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v2_collsp(A) & v3_collsp(A) & v4_collsp(A) & v2_anproj_2(A) & v3_anproj_2(A) & l1_collsp(A) ) => ( v6_anproj_2(A) <=> ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ! [H] : ( m1_subset_1(H,u1_struct_0(A)) => ! [I] : ( m1_subset_1(I,u1_struct_0(A)) => ! [J] : ( m1_subset_1(J,u1_struct_0(A)) => ! [K] : ( m1_subset_1(K,u1_struct_0(A)) => ( ( r1_collsp(A,B,C,D) & r1_collsp(A,B,C,E) & r1_collsp(A,B,F,G) & r1_collsp(A,B,F,H) & r1_collsp(A,C,G,K) & r1_collsp(A,F,D,K) & r1_collsp(A,C,H,J) & r1_collsp(A,E,F,J) & r1_collsp(A,D,H,I) & r1_collsp(A,E,G,I) ) => ( B = D | B = E | D = E | C = D | C = E | B = G | B = H | G = H | F = G | F = H | r1_collsp(A,B,C,F) | r1_collsp(A,I,J,K) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ), file(anproj_2,d13_anproj_2), [interesting(0.00)]). fof(d4_anproj_2,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ! [H] : ( m1_subset_1(H,u1_struct_0(A)) => ( r4_anproj_2(A,B,C,D,E,F,G,H) <=> ( ~ r2_anproj_1(A,B,C,F) & r2_anproj_1(A,B,C,D) & r2_anproj_1(A,B,C,E) & r2_anproj_1(A,B,F,G) & r2_anproj_1(A,B,F,H) ) ) ) ) ) ) ) ) ) ) ), file(anproj_2,d4_anproj_2), [interesting(0.00)]). fof(d5_anproj_2,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ! [H] : ( m1_subset_1(H,u1_struct_0(A)) => ( r5_anproj_2(A,B,C,D,E,F,G,H) <=> ( ~ r1_anproj_1(A,B,D) & ~ r1_anproj_1(A,B,E) & ~ r1_anproj_1(A,B,G) & ~ r1_anproj_1(A,B,H) & ~ r1_anproj_1(A,C,D) & ~ r1_anproj_1(A,C,E) & ~ r1_anproj_1(A,F,G) & ~ r1_anproj_1(A,F,H) & ~ r1_anproj_1(A,D,E) & ~ r1_anproj_1(A,G,H) ) ) ) ) ) ) ) ) ) ) ), file(anproj_2,d5_anproj_2), [interesting(0.00)]). fof(l29_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,k1_numbers) => ( k3_rlvect_1(A,B,D) = C => ( D = 0 | r1_anproj_1(A,B,C) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_rlvect_1,d2_anproj_1]), [file(anproj_2,l29_anproj_2),interesting(0.00)]). fof(t6_anproj_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( ( r1_anproj_1(A,B,C) & r1_anproj_1(A,C,D) ) => r1_anproj_1(A,B,D) ) ) ) ) ) ), file(anproj_1,t6_anproj_1), [interesting(0.00)]). fof(l33_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,k1_numbers) => ( ( k3_rlvect_1(A,B,D) = C & v8_rlvect_1(B,A) ) => ( D = 0 | v8_rlvect_1(C,A) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d13_rlvect_1,t24_rlvect_1,d13_rlvect_1]), [file(anproj_2,l33_anproj_2),interesting(0.00)]). fof(l30_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,k1_numbers) => ~ ( ~ r1_anproj_1(A,B,C) & D = k3_rlvect_1(A,C,E) & E != 0 & r1_anproj_1(A,B,D) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t5_anproj_1,d9_rlvect_1,t6_xcmplx_1,t5_anproj_1]), [file(anproj_2,l30_anproj_2),interesting(0.00)]). fof(t11_anproj_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( ( v8_rlvect_1(B,A) & v8_rlvect_1(C,A) ) => ( r1_anproj_1(A,B,C) | ( r2_anproj_1(A,B,C,D) <=> ? [E] : ( m1_subset_1(E,k1_numbers) & ? [F] : ( m1_subset_1(F,k1_numbers) & D = k4_rlvect_1(A,k3_rlvect_1(A,B,E),k3_rlvect_1(A,C,F)) ) ) ) ) ) ) ) ) ) ), file(anproj_1,t11_anproj_1), [interesting(0.00)]). fof(l31_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,k1_numbers) => ! [H] : ( m1_subset_1(H,k1_numbers) => ! [I] : ( m1_subset_1(I,k1_numbers) => ( ( B = k4_rlvect_1(A,k3_rlvect_1(A,C,G),k3_rlvect_1(A,D,H)) & D = k4_rlvect_1(A,E,k3_rlvect_1(A,F,I)) ) => B = k4_rlvect_1(A,k4_rlvect_1(A,k3_rlvect_1(A,E,H),k3_rlvect_1(A,C,G)),k3_rlvect_1(A,F,k4_real_1(H,I))) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_rlvect_1,d6_rlvect_1,d9_rlvect_1]), [file(anproj_2,l31_anproj_2),interesting(0.00)]). fof(l32_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,k1_numbers) => ! [H] : ( m1_subset_1(H,k1_numbers) => ! [I] : ( m1_subset_1(I,k1_numbers) => ( ( B = k4_rlvect_1(A,k3_rlvect_1(A,C,G),k3_rlvect_1(A,D,H)) & D = k4_rlvect_1(A,E,k3_rlvect_1(A,F,I)) ) => B = k4_rlvect_1(A,k4_rlvect_1(A,k3_rlvect_1(A,E,H),k3_rlvect_1(A,F,k4_real_1(H,I))),k3_rlvect_1(A,C,G)) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l31_anproj_2,d6_rlvect_1]), [file(anproj_2,l32_anproj_2),interesting(0.00)]). fof(l42_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,k1_numbers) => ! [H] : ( m1_subset_1(H,k1_numbers) => ! [I] : ( m1_subset_1(I,k1_numbers) => ! [J] : ( m1_subset_1(J,k1_numbers) => ! [K] : ( m1_subset_1(K,k1_numbers) => ! [L] : ( m1_subset_1(L,k1_numbers) => ( ( B = k4_rlvect_1(A,k4_rlvect_1(A,C,k3_rlvect_1(A,D,G)),k3_rlvect_1(A,E,H)) & F = k4_rlvect_1(A,k4_rlvect_1(A,k3_rlvect_1(A,C,K),k3_rlvect_1(A,D,I)),k3_rlvect_1(A,E,k4_real_1(K,H))) & K = L & I = k4_real_1(L,G) & k4_real_1(K,H) = J ) => F = k3_rlvect_1(A,B,K) ) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_rlvect_1,d9_rlvect_1,d9_rlvect_1,d9_rlvect_1]), [file(anproj_2,l42_anproj_2),interesting(0.00)]). fof(l34_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,k1_numbers) => ! [G] : ( m1_subset_1(G,k1_numbers) => ~ ( ~ r1_anproj_1(A,B,C) & D = k3_rlvect_1(A,C,F) & F != 0 & E = k3_rlvect_1(A,B,G) & G != 0 & r1_anproj_1(A,E,D) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t5_anproj_1,d9_rlvect_1,t6_xcmplx_1,d2_anproj_1]), [file(anproj_2,l34_anproj_2),interesting(0.00)]). fof(l35_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ! [H] : ( m1_subset_1(H,k1_numbers) => ! [I] : ( m1_subset_1(I,k1_numbers) => ! [J] : ( m1_subset_1(J,k1_numbers) => ! [K] : ( m1_subset_1(K,k1_numbers) => ( ( B = k4_rlvect_1(A,k3_rlvect_1(A,C,J),k3_rlvect_1(A,D,K)) & C = k4_rlvect_1(A,E,k3_rlvect_1(A,F,H)) & D = k4_rlvect_1(A,E,k3_rlvect_1(A,G,I)) ) => B = k4_rlvect_1(A,k4_rlvect_1(A,k3_rlvect_1(A,E,k3_real_1(J,K)),k3_rlvect_1(A,F,k4_real_1(J,H))),k3_rlvect_1(A,G,k4_real_1(K,I))) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_rlvect_1,d9_rlvect_1,d9_rlvect_1,d9_rlvect_1,d6_rlvect_1,d6_rlvect_1,d9_rlvect_1]), [file(anproj_2,l35_anproj_2),interesting(0.00)]). fof(t4_xcmplx_1,theorem,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ! [C] : ( v1_xcmplx_0(C) => k3_xcmplx_0(A,k3_xcmplx_0(B,C)) = k3_xcmplx_0(k3_xcmplx_0(A,B),C) ) ) ) ), file(xcmplx_1,t4_xcmplx_1), [interesting(0.00)]). fof(t8_xcmplx_1,theorem,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ! [C] : ( v1_xcmplx_0(C) => k3_xcmplx_0(A,k2_xcmplx_0(B,C)) = k2_xcmplx_0(k3_xcmplx_0(A,B),k3_xcmplx_0(A,C)) ) ) ) ), file(xcmplx_1,t8_xcmplx_1), [interesting(0.00)]). fof(l37_anproj_2,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,k1_numbers) => ! [D] : ( m1_subset_1(D,k1_numbers) => ! [E] : ( m1_subset_1(E,k1_numbers) => ! [F] : ( m1_subset_1(F,k1_numbers) => ! [G] : ( m1_subset_1(G,k1_numbers) => ! [H] : ( m1_subset_1(H,k1_numbers) => ( ( k3_real_1(E,G) = k3_real_1(F,H) & k4_real_1(E,A) = k4_real_1(F,B) & k4_real_1(G,C) = k4_real_1(H,D) ) => ( A = B | D = 0 | E = k4_real_1(k4_real_1(k5_real_1(k4_real_1(B,C),k4_real_1(B,D)),k2_real_1(k5_real_1(k4_real_1(B,D),k4_real_1(A,D)))),G) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t4_xcmplx_1,t8_xcmplx_1,t4_xcmplx_1,l36_anproj_2,d7_xcmplx_0]), [file(anproj_2,l37_anproj_2),interesting(0.00)]). fof(l38_anproj_2,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,k1_numbers) => ! [D] : ( m1_subset_1(D,k1_numbers) => ~ ( A != 0 & B != C & D != 0 & k4_real_1(D,k2_real_1(k5_real_1(k4_real_1(C,A),k4_real_1(B,A)))) = 0 ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l36_anproj_2,t203_xcmplx_1,t6_xcmplx_1]), [file(anproj_2,l38_anproj_2),interesting(0.00)]). fof(l40_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => k4_rlvect_1(A,k4_rlvect_1(A,k4_rlvect_1(A,B,C),D),k4_rlvect_1(A,k4_rlvect_1(A,E,F),G)) = k4_rlvect_1(A,k4_rlvect_1(A,k4_rlvect_1(A,B,E),k4_rlvect_1(A,C,F)),k4_rlvect_1(A,D,G)) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d6_rlvect_1,d6_rlvect_1,d6_rlvect_1,d6_rlvect_1,d6_rlvect_1,d6_rlvect_1]), [file(anproj_2,l40_anproj_2),interesting(0.00)]). fof(s9_funct_2,theorem, ( ! [A] : ( r2_hidden(A,f1_s9_funct_2) => ( ( p1_s9_funct_2(A) => r2_hidden(f3_s9_funct_2(A),f2_s9_funct_2) ) & ( ~ p1_s9_funct_2(A) => r2_hidden(f4_s9_funct_2(A),f2_s9_funct_2) ) ) ) => ? [A] : ( v1_funct_1(A) & v1_funct_2(A,f1_s9_funct_2,f2_s9_funct_2) & m2_relset_1(A,f1_s9_funct_2,f2_s9_funct_2) & ! [B] : ( r2_hidden(B,f1_s9_funct_2) => ( ( p1_s9_funct_2(B) => k1_funct_1(A,B) = f3_s9_funct_2(B) ) & ( ~ p1_s9_funct_2(B) => k1_funct_1(A,B) = f4_s9_funct_2(B) ) ) ) ) ), file(funct_2,s9_funct_2), [interesting(0.00)]). fof(t11_funct_2,theorem,( ! [A,B,C] : ( ( v1_funct_1(C) & v1_funct_2(C,A,B) & m2_relset_1(C,A,B) ) => ( ( B = k1_xboole_0 => A = k1_xboole_0 ) => r2_hidden(C,k1_funct_2(A,B)) ) ) ), file(funct_2,t11_funct_2), [interesting(0.00)]). fof(t10_anproj_2,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( m1_subset_1(C,A) => ! [D] : ( m1_subset_1(D,A) => ? [E] : ( m2_fraenkel(E,A,k1_numbers,k1_fraenkel(A,k1_numbers)) & ? [F] : ( m2_fraenkel(F,A,k1_numbers,k1_fraenkel(A,k1_numbers)) & ? [G] : ( m2_fraenkel(G,A,k1_numbers,k1_fraenkel(A,k1_numbers)) & ! [H] : ( r2_hidden(H,A) => ( ( H = B => k1_funct_1(E,H) = 1 ) & ( H != B => k1_funct_1(E,H) = 0 ) ) ) & ! [H] : ( r2_hidden(H,A) => ( ( H = C => k1_funct_1(F,H) = 1 ) & ( H != C => k1_funct_1(F,H) = 0 ) ) ) & ! [H] : ( r2_hidden(H,A) => ( ( H = D => k1_funct_1(G,H) = 1 ) & ( H != D => k1_funct_1(G,H) = 0 ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[s9_funct_2,s9_funct_2,s9_funct_2,t11_funct_2]), [file(anproj_2,t10_anproj_2),interesting(0.00)]). fof(t13_funcsdom,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => k8_funct_2(A,k1_numbers,k9_funcsdom(A),B) = 0 ) ) ), file(funcsdom,t13_funcsdom), [interesting(0.00)]). fof(t10_funcsdom,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k1_numbers,k1_fraenkel(A,k1_numbers)) => ! [C] : ( m2_fraenkel(C,A,k1_numbers,k1_fraenkel(A,k1_numbers)) => ! [D] : ( m2_fraenkel(D,A,k1_numbers,k1_fraenkel(A,k1_numbers)) => ( B = k1_funcsdom(A,k1_numbers,k6_funcsdom(A),C,D) <=> ! [E] : ( m1_subset_1(E,A) => k8_funct_2(A,k1_numbers,B,E) = k3_real_1(k8_funct_2(A,k1_numbers,C,E),k8_funct_2(A,k1_numbers,D,E)) ) ) ) ) ) ) ), file(funcsdom,t10_funcsdom), [interesting(0.00)]). fof(t15_funcsdom,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k1_numbers,k1_fraenkel(A,k1_numbers)) => ! [C] : ( m2_fraenkel(C,A,k1_numbers,k1_fraenkel(A,k1_numbers)) => ! [D] : ( m1_subset_1(D,k1_numbers) => ( B = k2_funcsdom(A,k1_numbers,k1_numbers,k1_fraenkel(A,k1_numbers),k8_funcsdom(A),k1_domain_1(k1_numbers,k1_fraenkel(A,k1_numbers),D,C)) <=> ! [E] : ( m1_subset_1(E,A) => k8_funct_2(A,k1_numbers,B,E) = k4_real_1(D,k8_funct_2(A,k1_numbers,C,E)) ) ) ) ) ) ) ), file(funcsdom,t15_funcsdom), [interesting(0.00)]). fof(t11_anproj_2,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k1_numbers,k1_fraenkel(A,k1_numbers)) => ! [C] : ( m2_fraenkel(C,A,k1_numbers,k1_fraenkel(A,k1_numbers)) => ! [D] : ( m2_fraenkel(D,A,k1_numbers,k1_fraenkel(A,k1_numbers)) => ! [E] : ( m1_subset_1(E,A) => ! [F] : ( m1_subset_1(F,A) => ! [G] : ( m1_subset_1(G,A) => ( ( r2_hidden(E,A) & r2_hidden(F,A) & r2_hidden(G,A) & ! [H] : ( r2_hidden(H,A) => ( ( H = E => k1_funct_1(B,H) = 1 ) & ( H != E => k1_funct_1(B,H) = 0 ) ) ) & ! [H] : ( r2_hidden(H,A) => ( ( H = F => k1_funct_1(C,H) = 1 ) & ( H != F => k1_funct_1(C,H) = 0 ) ) ) & ! [H] : ( r2_hidden(H,A) => ( ( H = G => k1_funct_1(D,H) = 1 ) & ( H != G => k1_funct_1(D,H) = 0 ) ) ) ) => ( E = F | E = G | F = G | ! [H] : ( m1_subset_1(H,k1_numbers) => ! [I] : ( m1_subset_1(I,k1_numbers) => ! [J] : ( m1_subset_1(J,k1_numbers) => ( k1_funcsdom(A,k1_numbers,k6_funcsdom(A),k1_funcsdom(A,k1_numbers,k6_funcsdom(A),k2_funcsdom(A,k1_numbers,k1_numbers,k1_fraenkel(A,k1_numbers),k8_funcsdom(A),k1_domain_1(k1_numbers,k1_fraenkel(A,k1_numbers),H,B)),k2_funcsdom(A,k1_numbers,k1_numbers,k1_fraenkel(A,k1_numbers),k8_funcsdom(A),k1_domain_1(k1_numbers,k1_fraenkel(A,k1_numbers),I,C))),k2_funcsdom(A,k1_numbers,k1_numbers,k1_fraenkel(A,k1_numbers),k8_funcsdom(A),k1_domain_1(k1_numbers,k1_fraenkel(A,k1_numbers),J,D))) = k9_funcsdom(A) => ( H = 0 & I = 0 & J = 0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t13_funcsdom,t10_funcsdom,t10_funcsdom,t15_funcsdom,t15_funcsdom,t15_funcsdom,t13_funcsdom,t10_funcsdom,t10_funcsdom,t15_funcsdom,t15_funcsdom,t15_funcsdom,t13_funcsdom,t10_funcsdom,t10_funcsdom,t15_funcsdom,t15_funcsdom,t15_funcsdom]), [file(anproj_2,t11_anproj_2),interesting(0.00)]). fof(t12_anproj_2,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( m1_subset_1(C,A) => ! [D] : ( m1_subset_1(D,A) => ~ ( r2_hidden(B,A) & r2_hidden(C,A) & r2_hidden(D,A) & B != C & B != D & C != D & ! [E] : ( m2_fraenkel(E,A,k1_numbers,k1_fraenkel(A,k1_numbers)) => ! [F] : ( m2_fraenkel(F,A,k1_numbers,k1_fraenkel(A,k1_numbers)) => ! [G] : ( m2_fraenkel(G,A,k1_numbers,k1_fraenkel(A,k1_numbers)) => ? [H] : ( m1_subset_1(H,k1_numbers) & ? [I] : ( m1_subset_1(I,k1_numbers) & ? [J] : ( m1_subset_1(J,k1_numbers) & k1_funcsdom(A,k1_numbers,k6_funcsdom(A),k1_funcsdom(A,k1_numbers,k6_funcsdom(A),k2_funcsdom(A,k1_numbers,k1_numbers,k1_fraenkel(A,k1_numbers),k8_funcsdom(A),k1_domain_1(k1_numbers,k1_fraenkel(A,k1_numbers),H,E)),k2_funcsdom(A,k1_numbers,k1_numbers,k1_fraenkel(A,k1_numbers),k8_funcsdom(A),k1_domain_1(k1_numbers,k1_fraenkel(A,k1_numbers),I,F))),k2_funcsdom(A,k1_numbers,k1_numbers,k1_fraenkel(A,k1_numbers),k8_funcsdom(A),k1_domain_1(k1_numbers,k1_fraenkel(A,k1_numbers),J,G))) = k9_funcsdom(A) & ~ ( H = 0 & I = 0 & J = 0 ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t10_anproj_2,t11_anproj_2]), [file(anproj_2,t12_anproj_2),interesting(0.00)]). fof(d1_enumset1,definition,( ! [A,B,C,D] : ( D = k1_enumset1(A,B,C) <=> ! [E] : ( r2_hidden(E,D) <=> ~ ( E != A & E != B & E != C ) ) ) ), file(enumset1,d1_enumset1), [interesting(0.00)]). fof(t113_funct_2,theorem,( ! [A,B,C] : ( ( v1_funct_1(C) & v1_funct_2(C,A,B) & m2_relset_1(C,A,B) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,A,B) & m2_relset_1(D,A,B) ) => ( ! [E] : ( m1_subset_1(E,A) => k1_funct_1(C,E) = k1_funct_1(D,E) ) => C = D ) ) ) ), file(funct_2,t113_funct_2), [interesting(0.00)]). fof(t13_anproj_2,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k1_numbers,k1_fraenkel(A,k1_numbers)) => ! [C] : ( m2_fraenkel(C,A,k1_numbers,k1_fraenkel(A,k1_numbers)) => ! [D] : ( m2_fraenkel(D,A,k1_numbers,k1_fraenkel(A,k1_numbers)) => ! [E] : ( m1_subset_1(E,A) => ! [F] : ( m1_subset_1(F,A) => ! [G] : ( m1_subset_1(G,A) => ( ( A = k8_domain_1(A,E,F,G) & ! [H] : ( r2_hidden(H,A) => ( ( H = E => k1_funct_1(B,H) = 1 ) & ( H != E => k1_funct_1(B,H) = 0 ) ) ) & ! [H] : ( r2_hidden(H,A) => ( ( H = F => k1_funct_1(C,H) = 1 ) & ( H != F => k1_funct_1(C,H) = 0 ) ) ) & ! [H] : ( r2_hidden(H,A) => ( ( H = G => k1_funct_1(D,H) = 1 ) & ( H != G => k1_funct_1(D,H) = 0 ) ) ) ) => ( E = F | E = G | F = G | ! [H] : ( m2_fraenkel(H,A,k1_numbers,k1_fraenkel(A,k1_numbers)) => ? [I] : ( m1_subset_1(I,k1_numbers) & ? [J] : ( m1_subset_1(J,k1_numbers) & ? [K] : ( m1_subset_1(K,k1_numbers) & H = k1_funcsdom(A,k1_numbers,k6_funcsdom(A),k1_funcsdom(A,k1_numbers,k6_funcsdom(A),k2_funcsdom(A,k1_numbers,k1_numbers,k1_fraenkel(A,k1_numbers),k8_funcsdom(A),k1_domain_1(k1_numbers,k1_fraenkel(A,k1_numbers),I,B)),k2_funcsdom(A,k1_numbers,k1_numbers,k1_fraenkel(A,k1_numbers),k8_funcsdom(A),k1_domain_1(k1_numbers,k1_fraenkel(A,k1_numbers),J,C))),k2_funcsdom(A,k1_numbers,k1_numbers,k1_fraenkel(A,k1_numbers),k8_funcsdom(A),k1_domain_1(k1_numbers,k1_fraenkel(A,k1_numbers),K,D))) ) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_enumset1,t10_funcsdom,t10_funcsdom,t15_funcsdom,t15_funcsdom,t15_funcsdom,t10_funcsdom,t10_funcsdom,t15_funcsdom,t15_funcsdom,t15_funcsdom,t10_funcsdom,t10_funcsdom,t15_funcsdom,t15_funcsdom,t15_funcsdom,t113_funct_2]), [file(anproj_2,t13_anproj_2),interesting(0.00)]). fof(t14_anproj_2,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( m1_subset_1(C,A) => ! [D] : ( m1_subset_1(D,A) => ~ ( A = k8_domain_1(A,B,C,D) & B != C & B != D & C != D & ! [E] : ( m2_fraenkel(E,A,k1_numbers,k1_fraenkel(A,k1_numbers)) => ! [F] : ( m2_fraenkel(F,A,k1_numbers,k1_fraenkel(A,k1_numbers)) => ! [G] : ( m2_fraenkel(G,A,k1_numbers,k1_fraenkel(A,k1_numbers)) => ? [H] : ( m2_fraenkel(H,A,k1_numbers,k1_fraenkel(A,k1_numbers)) & ! [I] : ( m1_subset_1(I,k1_numbers) => ! [J] : ( m1_subset_1(J,k1_numbers) => ! [K] : ( m1_subset_1(K,k1_numbers) => H != k1_funcsdom(A,k1_numbers,k6_funcsdom(A),k1_funcsdom(A,k1_numbers,k6_funcsdom(A),k2_funcsdom(A,k1_numbers,k1_numbers,k1_fraenkel(A,k1_numbers),k8_funcsdom(A),k1_domain_1(k1_numbers,k1_fraenkel(A,k1_numbers),I,E)),k2_funcsdom(A,k1_numbers,k1_numbers,k1_fraenkel(A,k1_numbers),k8_funcsdom(A),k1_domain_1(k1_numbers,k1_fraenkel(A,k1_numbers),J,F))),k2_funcsdom(A,k1_numbers,k1_numbers,k1_fraenkel(A,k1_numbers),k8_funcsdom(A),k1_domain_1(k1_numbers,k1_fraenkel(A,k1_numbers),K,G))) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t10_anproj_2,t13_anproj_2]), [file(anproj_2,t14_anproj_2),interesting(0.00)]). fof(t15_anproj_2,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( m1_subset_1(C,A) => ! [D] : ( m1_subset_1(D,A) => ~ ( A = k8_domain_1(A,B,C,D) & B != C & B != D & C != D & ! [E] : ( m2_fraenkel(E,A,k1_numbers,k1_fraenkel(A,k1_numbers)) => ! [F] : ( m2_fraenkel(F,A,k1_numbers,k1_fraenkel(A,k1_numbers)) => ! [G] : ( m2_fraenkel(G,A,k1_numbers,k1_fraenkel(A,k1_numbers)) => ~ ( ! [H] : ( m1_subset_1(H,k1_numbers) => ! [I] : ( m1_subset_1(I,k1_numbers) => ! [J] : ( m1_subset_1(J,k1_numbers) => ( k1_funcsdom(A,k1_numbers,k6_funcsdom(A),k1_funcsdom(A,k1_numbers,k6_funcsdom(A),k2_funcsdom(A,k1_numbers,k1_numbers,k1_fraenkel(A,k1_numbers),k8_funcsdom(A),k1_domain_1(k1_numbers,k1_fraenkel(A,k1_numbers),H,E)),k2_funcsdom(A,k1_numbers,k1_numbers,k1_fraenkel(A,k1_numbers),k8_funcsdom(A),k1_domain_1(k1_numbers,k1_fraenkel(A,k1_numbers),I,F))),k2_funcsdom(A,k1_numbers,k1_numbers,k1_fraenkel(A,k1_numbers),k8_funcsdom(A),k1_domain_1(k1_numbers,k1_fraenkel(A,k1_numbers),J,G))) = k9_funcsdom(A) => ( H = 0 & I = 0 & J = 0 ) ) ) ) ) & ! [H] : ( m2_fraenkel(H,A,k1_numbers,k1_fraenkel(A,k1_numbers)) => ? [I] : ( m1_subset_1(I,k1_numbers) & ? [J] : ( m1_subset_1(J,k1_numbers) & ? [K] : ( m1_subset_1(K,k1_numbers) & H = k1_funcsdom(A,k1_numbers,k6_funcsdom(A),k1_funcsdom(A,k1_numbers,k6_funcsdom(A),k2_funcsdom(A,k1_numbers,k1_numbers,k1_fraenkel(A,k1_numbers),k8_funcsdom(A),k1_domain_1(k1_numbers,k1_fraenkel(A,k1_numbers),I,E)),k2_funcsdom(A,k1_numbers,k1_numbers,k1_fraenkel(A,k1_numbers),k8_funcsdom(A),k1_domain_1(k1_numbers,k1_fraenkel(A,k1_numbers),J,F))),k2_funcsdom(A,k1_numbers,k1_numbers,k1_fraenkel(A,k1_numbers),k8_funcsdom(A),k1_domain_1(k1_numbers,k1_fraenkel(A,k1_numbers),K,G))) ) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t10_anproj_2,t11_anproj_2,t13_anproj_2]), [file(anproj_2,t15_anproj_2),interesting(0.00)]). fof(d7_funcsdom,definition,( ! [A] : ( ~ v1_xboole_0(A) => k11_funcsdom(A) = g2_rlvect_1(k1_fraenkel(A,k1_numbers),k9_funcsdom(A),k6_funcsdom(A),k8_funcsdom(A)) ) ), file(funcsdom,d7_funcsdom), [interesting(0.00)]). fof(d4_rlvect_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,k1_numbers) => k3_rlvect_1(A,B,C) = k8_funct_2(k2_zfmisc_1(k1_numbers,u1_struct_0(A)),u1_struct_0(A),u2_rlvect_1(A),k1_domain_1(k1_numbers,u1_struct_0(A),C,B)) ) ) ) ), file(rlvect_1,d4_rlvect_1), [interesting(0.00)]). fof(d3_rlvect_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => k2_rlvect_1(A,B,C) = k8_funct_2(k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A),u1_rlvect_1(A),k1_domain_1(u1_struct_0(A),u1_struct_0(A),B,C)) ) ) ) ), file(rlvect_1,d3_rlvect_1), [interesting(0.00)]). fof(d2_rlvect_1,definition,( ! [A] : ( l2_struct_0(A) => k1_rlvect_1(A) = u2_struct_0(A) ) ), file(rlvect_1,d2_rlvect_1), [interesting(0.00)]). fof(d8_anproj_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l2_struct_0(A) ) => ( v3_realset2(A) <=> ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => B = k1_rlvect_1(A) ) ) ) ), file(anproj_1,d8_anproj_1), [interesting(0.00)]). fof(t16_anproj_2,theorem,( ? [A] : ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & ~ v3_realset2(A) & l2_rlvect_1(A) & ? [B] : ( m1_subset_1(B,u1_struct_0(A)) & ? [C] : ( m1_subset_1(C,u1_struct_0(A)) & ? [D] : ( m1_subset_1(D,u1_struct_0(A)) & ! [E] : ( m1_subset_1(E,k1_numbers) => ! [F] : ( m1_subset_1(F,k1_numbers) => ! [G] : ( m1_subset_1(G,k1_numbers) => ( k4_rlvect_1(A,k4_rlvect_1(A,k3_rlvect_1(A,B,E),k3_rlvect_1(A,C,F)),k3_rlvect_1(A,D,G)) = k1_rlvect_1(A) => ( E = 0 & F = 0 & G = 0 ) ) ) ) ) & ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ? [F] : ( m1_subset_1(F,k1_numbers) & ? [G] : ( m1_subset_1(G,k1_numbers) & ? [H] : ( m1_subset_1(H,k1_numbers) & E = k4_rlvect_1(A,k4_rlvect_1(A,k3_rlvect_1(A,B,F),k3_rlvect_1(A,C,G)),k3_rlvect_1(A,D,H)) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l50_anproj_2,t15_anproj_2,d7_funcsdom,d4_rlvect_1,d3_rlvect_1,d3_rlvect_1,d2_rlvect_1,d4_rlvect_1,d3_rlvect_1,d3_rlvect_1,t1_anproj_2,d13_rlvect_1,d8_anproj_1]), [file(anproj_2,t16_anproj_2),interesting(0.00)]). fof(t17_anproj_2,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( m1_subset_1(C,A) => ! [D] : ( m1_subset_1(D,A) => ! [E] : ( m1_subset_1(E,A) => ? [F] : ( m2_fraenkel(F,A,k1_numbers,k1_fraenkel(A,k1_numbers)) & ? [G] : ( m2_fraenkel(G,A,k1_numbers,k1_fraenkel(A,k1_numbers)) & ? [H] : ( m2_fraenkel(H,A,k1_numbers,k1_fraenkel(A,k1_numbers)) & ? [I] : ( m2_fraenkel(I,A,k1_numbers,k1_fraenkel(A,k1_numbers)) & ! [J] : ( r2_hidden(J,A) => ( ( J = B => k1_funct_1(F,J) = 1 ) & ( J != B => k1_funct_1(F,J) = 0 ) ) ) & ! [J] : ( r2_hidden(J,A) => ( ( J = C => k1_funct_1(G,J) = 1 ) & ( J != C => k1_funct_1(G,J) = 0 ) ) ) & ! [J] : ( r2_hidden(J,A) => ( ( J = D => k1_funct_1(H,J) = 1 ) & ( J != D => k1_funct_1(H,J) = 0 ) ) ) & ! [J] : ( r2_hidden(J,A) => ( ( J = E => k1_funct_1(I,J) = 1 ) & ( J != E => k1_funct_1(I,J) = 0 ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[s9_funct_2,s9_funct_2,s9_funct_2,s9_funct_2,t11_funct_2]), [file(anproj_2,t17_anproj_2),interesting(0.00)]). fof(t18_anproj_2,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k1_numbers,k1_fraenkel(A,k1_numbers)) => ! [C] : ( m2_fraenkel(C,A,k1_numbers,k1_fraenkel(A,k1_numbers)) => ! [D] : ( m2_fraenkel(D,A,k1_numbers,k1_fraenkel(A,k1_numbers)) => ! [E] : ( m2_fraenkel(E,A,k1_numbers,k1_fraenkel(A,k1_numbers)) => ! [F] : ( m1_subset_1(F,A) => ! [G] : ( m1_subset_1(G,A) => ! [H] : ( m1_subset_1(H,A) => ! [I] : ( m1_subset_1(I,A) => ( ( r2_hidden(F,A) & r2_hidden(G,A) & r2_hidden(H,A) & r2_hidden(I,A) & ! [J] : ( r2_hidden(J,A) => ( ( J = F => k1_funct_1(B,J) = 1 ) & ( J != F => k1_funct_1(B,J) = 0 ) ) ) & ! [J] : ( r2_hidden(J,A) => ( ( J = G => k1_funct_1(C,J) = 1 ) & ( J != G => k1_funct_1(C,J) = 0 ) ) ) & ! [J] : ( r2_hidden(J,A) => ( ( J = H => k1_funct_1(D,J) = 1 ) & ( J != H => k1_funct_1(D,J) = 0 ) ) ) & ! [J] : ( r2_hidden(J,A) => ( ( J = I => k1_funct_1(E,J) = 1 ) & ( J != I => k1_funct_1(E,J) = 0 ) ) ) ) => ( F = G | F = H | F = I | G = H | G = I | H = I | ! [J] : ( m1_subset_1(J,k1_numbers) => ! [K] : ( m1_subset_1(K,k1_numbers) => ! [L] : ( m1_subset_1(L,k1_numbers) => ! [M] : ( m1_subset_1(M,k1_numbers) => ( k1_funcsdom(A,k1_numbers,k6_funcsdom(A),k1_funcsdom(A,k1_numbers,k6_funcsdom(A),k1_funcsdom(A,k1_numbers,k6_funcsdom(A),k2_funcsdom(A,k1_numbers,k1_numbers,k1_fraenkel(A,k1_numbers),k8_funcsdom(A),k1_domain_1(k1_numbers,k1_fraenkel(A,k1_numbers),J,B)),k2_funcsdom(A,k1_numbers,k1_numbers,k1_fraenkel(A,k1_numbers),k8_funcsdom(A),k1_domain_1(k1_numbers,k1_fraenkel(A,k1_numbers),K,C))),k2_funcsdom(A,k1_numbers,k1_numbers,k1_fraenkel(A,k1_numbers),k8_funcsdom(A),k1_domain_1(k1_numbers,k1_fraenkel(A,k1_numbers),L,D))),k2_funcsdom(A,k1_numbers,k1_numbers,k1_fraenkel(A,k1_numbers),k8_funcsdom(A),k1_domain_1(k1_numbers,k1_fraenkel(A,k1_numbers),M,E))) = k9_funcsdom(A) => ( J = 0 & K = 0 & L = 0 & M = 0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t13_funcsdom,t10_funcsdom,t10_funcsdom,t10_funcsdom,t15_funcsdom,t15_funcsdom,t15_funcsdom,t15_funcsdom,t13_funcsdom,t10_funcsdom,t10_funcsdom,t10_funcsdom,t15_funcsdom,t15_funcsdom,t15_funcsdom,t15_funcsdom,t13_funcsdom,t10_funcsdom,t10_funcsdom,t10_funcsdom,t15_funcsdom,t15_funcsdom,t15_funcsdom,t15_funcsdom,t13_funcsdom,t10_funcsdom,t10_funcsdom,t10_funcsdom,t15_funcsdom,t15_funcsdom,t15_funcsdom,t15_funcsdom]), [file(anproj_2,t18_anproj_2),interesting(0.00)]). fof(t19_anproj_2,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( m1_subset_1(C,A) => ! [D] : ( m1_subset_1(D,A) => ! [E] : ( m1_subset_1(E,A) => ~ ( r2_hidden(B,A) & r2_hidden(C,A) & r2_hidden(D,A) & r2_hidden(E,A) & B != C & B != D & B != E & C != D & C != E & D != E & ! [F] : ( m2_fraenkel(F,A,k1_numbers,k1_fraenkel(A,k1_numbers)) => ! [G] : ( m2_fraenkel(G,A,k1_numbers,k1_fraenkel(A,k1_numbers)) => ! [H] : ( m2_fraenkel(H,A,k1_numbers,k1_fraenkel(A,k1_numbers)) => ! [I] : ( m2_fraenkel(I,A,k1_numbers,k1_fraenkel(A,k1_numbers)) => ? [J] : ( m1_subset_1(J,k1_numbers) & ? [K] : ( m1_subset_1(K,k1_numbers) & ? [L] : ( m1_subset_1(L,k1_numbers) & ? [M] : ( m1_subset_1(M,k1_numbers) & k1_funcsdom(A,k1_numbers,k6_funcsdom(A),k1_funcsdom(A,k1_numbers,k6_funcsdom(A),k1_funcsdom(A,k1_numbers,k6_funcsdom(A),k2_funcsdom(A,k1_numbers,k1_numbers,k1_fraenkel(A,k1_numbers),k8_funcsdom(A),k1_domain_1(k1_numbers,k1_fraenkel(A,k1_numbers),J,F)),k2_funcsdom(A,k1_numbers,k1_numbers,k1_fraenkel(A,k1_numbers),k8_funcsdom(A),k1_domain_1(k1_numbers,k1_fraenkel(A,k1_numbers),K,G))),k2_funcsdom(A,k1_numbers,k1_numbers,k1_fraenkel(A,k1_numbers),k8_funcsdom(A),k1_domain_1(k1_numbers,k1_fraenkel(A,k1_numbers),L,H))),k2_funcsdom(A,k1_numbers,k1_numbers,k1_fraenkel(A,k1_numbers),k8_funcsdom(A),k1_domain_1(k1_numbers,k1_fraenkel(A,k1_numbers),M,I))) = k9_funcsdom(A) & ~ ( J = 0 & K = 0 & L = 0 & M = 0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t17_anproj_2,t18_anproj_2]), [file(anproj_2,t19_anproj_2),interesting(0.00)]). fof(d2_enumset1,definition,( ! [A,B,C,D,E] : ( E = k2_enumset1(A,B,C,D) <=> ! [F] : ( r2_hidden(F,E) <=> ~ ( F != A & F != B & F != C & F != D ) ) ) ), file(enumset1,d2_enumset1), [interesting(0.00)]). fof(t20_anproj_2,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k1_numbers,k1_fraenkel(A,k1_numbers)) => ! [C] : ( m2_fraenkel(C,A,k1_numbers,k1_fraenkel(A,k1_numbers)) => ! [D] : ( m2_fraenkel(D,A,k1_numbers,k1_fraenkel(A,k1_numbers)) => ! [E] : ( m2_fraenkel(E,A,k1_numbers,k1_fraenkel(A,k1_numbers)) => ! [F] : ( m1_subset_1(F,A) => ! [G] : ( m1_subset_1(G,A) => ! [H] : ( m1_subset_1(H,A) => ! [I] : ( m1_subset_1(I,A) => ( ( A = k9_domain_1(A,F,G,H,I) & ! [J] : ( r2_hidden(J,A) => ( ( J = F => k1_funct_1(B,J) = 1 ) & ( J != F => k1_funct_1(B,J) = 0 ) ) ) & ! [J] : ( r2_hidden(J,A) => ( ( J = G => k1_funct_1(C,J) = 1 ) & ( J != G => k1_funct_1(C,J) = 0 ) ) ) & ! [J] : ( r2_hidden(J,A) => ( ( J = H => k1_funct_1(D,J) = 1 ) & ( J != H => k1_funct_1(D,J) = 0 ) ) ) & ! [J] : ( r2_hidden(J,A) => ( ( J = I => k1_funct_1(E,J) = 1 ) & ( J != I => k1_funct_1(E,J) = 0 ) ) ) ) => ( F = G | F = H | F = I | G = H | G = I | H = I | ! [J] : ( m2_fraenkel(J,A,k1_numbers,k1_fraenkel(A,k1_numbers)) => ? [K] : ( m1_subset_1(K,k1_numbers) & ? [L] : ( m1_subset_1(L,k1_numbers) & ? [M] : ( m1_subset_1(M,k1_numbers) & ? [N] : ( m1_subset_1(N,k1_numbers) & J = k1_funcsdom(A,k1_numbers,k6_funcsdom(A),k1_funcsdom(A,k1_numbers,k6_funcsdom(A),k1_funcsdom(A,k1_numbers,k6_funcsdom(A),k2_funcsdom(A,k1_numbers,k1_numbers,k1_fraenkel(A,k1_numbers),k8_funcsdom(A),k1_domain_1(k1_numbers,k1_fraenkel(A,k1_numbers),K,B)),k2_funcsdom(A,k1_numbers,k1_numbers,k1_fraenkel(A,k1_numbers),k8_funcsdom(A),k1_domain_1(k1_numbers,k1_fraenkel(A,k1_numbers),L,C))),k2_funcsdom(A,k1_numbers,k1_numbers,k1_fraenkel(A,k1_numbers),k8_funcsdom(A),k1_domain_1(k1_numbers,k1_fraenkel(A,k1_numbers),M,D))),k2_funcsdom(A,k1_numbers,k1_numbers,k1_fraenkel(A,k1_numbers),k8_funcsdom(A),k1_domain_1(k1_numbers,k1_fraenkel(A,k1_numbers),N,E))) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_enumset1,t10_funcsdom,t10_funcsdom,t10_funcsdom,t15_funcsdom,t15_funcsdom,t15_funcsdom,t15_funcsdom,t10_funcsdom,t10_funcsdom,t10_funcsdom,t15_funcsdom,t15_funcsdom,t15_funcsdom,t15_funcsdom,t10_funcsdom,t10_funcsdom,t10_funcsdom,t15_funcsdom,t15_funcsdom,t15_funcsdom,t15_funcsdom,t10_funcsdom,t10_funcsdom,t10_funcsdom,t15_funcsdom,t15_funcsdom,t15_funcsdom,t15_funcsdom,t113_funct_2]), [file(anproj_2,t20_anproj_2),interesting(0.00)]). fof(t21_anproj_2,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( m1_subset_1(C,A) => ! [D] : ( m1_subset_1(D,A) => ! [E] : ( m1_subset_1(E,A) => ~ ( A = k9_domain_1(A,B,C,D,E) & B != C & B != D & B != E & C != D & C != E & D != E & ! [F] : ( m2_fraenkel(F,A,k1_numbers,k1_fraenkel(A,k1_numbers)) => ! [G] : ( m2_fraenkel(G,A,k1_numbers,k1_fraenkel(A,k1_numbers)) => ! [H] : ( m2_fraenkel(H,A,k1_numbers,k1_fraenkel(A,k1_numbers)) => ! [I] : ( m2_fraenkel(I,A,k1_numbers,k1_fraenkel(A,k1_numbers)) => ? [J] : ( m2_fraenkel(J,A,k1_numbers,k1_fraenkel(A,k1_numbers)) & ! [K] : ( m1_subset_1(K,k1_numbers) => ! [L] : ( m1_subset_1(L,k1_numbers) => ! [M] : ( m1_subset_1(M,k1_numbers) => ! [N] : ( m1_subset_1(N,k1_numbers) => J != k1_funcsdom(A,k1_numbers,k6_funcsdom(A),k1_funcsdom(A,k1_numbers,k6_funcsdom(A),k1_funcsdom(A,k1_numbers,k6_funcsdom(A),k2_funcsdom(A,k1_numbers,k1_numbers,k1_fraenkel(A,k1_numbers),k8_funcsdom(A),k1_domain_1(k1_numbers,k1_fraenkel(A,k1_numbers),K,F)),k2_funcsdom(A,k1_numbers,k1_numbers,k1_fraenkel(A,k1_numbers),k8_funcsdom(A),k1_domain_1(k1_numbers,k1_fraenkel(A,k1_numbers),L,G))),k2_funcsdom(A,k1_numbers,k1_numbers,k1_fraenkel(A,k1_numbers),k8_funcsdom(A),k1_domain_1(k1_numbers,k1_fraenkel(A,k1_numbers),M,H))),k2_funcsdom(A,k1_numbers,k1_numbers,k1_fraenkel(A,k1_numbers),k8_funcsdom(A),k1_domain_1(k1_numbers,k1_fraenkel(A,k1_numbers),N,I))) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t17_anproj_2,t20_anproj_2]), [file(anproj_2,t21_anproj_2),interesting(0.00)]). fof(t22_anproj_2,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( m1_subset_1(C,A) => ! [D] : ( m1_subset_1(D,A) => ! [E] : ( m1_subset_1(E,A) => ~ ( A = k9_domain_1(A,B,C,D,E) & B != C & B != D & B != E & C != D & C != E & D != E & ! [F] : ( m2_fraenkel(F,A,k1_numbers,k1_fraenkel(A,k1_numbers)) => ! [G] : ( m2_fraenkel(G,A,k1_numbers,k1_fraenkel(A,k1_numbers)) => ! [H] : ( m2_fraenkel(H,A,k1_numbers,k1_fraenkel(A,k1_numbers)) => ! [I] : ( m2_fraenkel(I,A,k1_numbers,k1_fraenkel(A,k1_numbers)) => ~ ( ! [J] : ( m1_subset_1(J,k1_numbers) => ! [K] : ( m1_subset_1(K,k1_numbers) => ! [L] : ( m1_subset_1(L,k1_numbers) => ! [M] : ( m1_subset_1(M,k1_numbers) => ( k1_funcsdom(A,k1_numbers,k6_funcsdom(A),k1_funcsdom(A,k1_numbers,k6_funcsdom(A),k1_funcsdom(A,k1_numbers,k6_funcsdom(A),k2_funcsdom(A,k1_numbers,k1_numbers,k1_fraenkel(A,k1_numbers),k8_funcsdom(A),k1_domain_1(k1_numbers,k1_fraenkel(A,k1_numbers),J,F)),k2_funcsdom(A,k1_numbers,k1_numbers,k1_fraenkel(A,k1_numbers),k8_funcsdom(A),k1_domain_1(k1_numbers,k1_fraenkel(A,k1_numbers),K,G))),k2_funcsdom(A,k1_numbers,k1_numbers,k1_fraenkel(A,k1_numbers),k8_funcsdom(A),k1_domain_1(k1_numbers,k1_fraenkel(A,k1_numbers),L,H))),k2_funcsdom(A,k1_numbers,k1_numbers,k1_fraenkel(A,k1_numbers),k8_funcsdom(A),k1_domain_1(k1_numbers,k1_fraenkel(A,k1_numbers),M,I))) = k9_funcsdom(A) => ( J = 0 & K = 0 & L = 0 & M = 0 ) ) ) ) ) ) & ! [J] : ( m2_fraenkel(J,A,k1_numbers,k1_fraenkel(A,k1_numbers)) => ? [K] : ( m1_subset_1(K,k1_numbers) & ? [L] : ( m1_subset_1(L,k1_numbers) & ? [M] : ( m1_subset_1(M,k1_numbers) & ? [N] : ( m1_subset_1(N,k1_numbers) & J = k1_funcsdom(A,k1_numbers,k6_funcsdom(A),k1_funcsdom(A,k1_numbers,k6_funcsdom(A),k1_funcsdom(A,k1_numbers,k6_funcsdom(A),k2_funcsdom(A,k1_numbers,k1_numbers,k1_fraenkel(A,k1_numbers),k8_funcsdom(A),k1_domain_1(k1_numbers,k1_fraenkel(A,k1_numbers),K,F)),k2_funcsdom(A,k1_numbers,k1_numbers,k1_fraenkel(A,k1_numbers),k8_funcsdom(A),k1_domain_1(k1_numbers,k1_fraenkel(A,k1_numbers),L,G))),k2_funcsdom(A,k1_numbers,k1_numbers,k1_fraenkel(A,k1_numbers),k8_funcsdom(A),k1_domain_1(k1_numbers,k1_fraenkel(A,k1_numbers),M,H))),k2_funcsdom(A,k1_numbers,k1_numbers,k1_fraenkel(A,k1_numbers),k8_funcsdom(A),k1_domain_1(k1_numbers,k1_fraenkel(A,k1_numbers),N,I))) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t17_anproj_2,t18_anproj_2,t20_anproj_2]), [file(anproj_2,t22_anproj_2),interesting(0.00)]). fof(t23_anproj_2,theorem,( ? [A] : ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & ~ v3_realset2(A) & l2_rlvect_1(A) & ? [B] : ( m1_subset_1(B,u1_struct_0(A)) & ? [C] : ( m1_subset_1(C,u1_struct_0(A)) & ? [D] : ( m1_subset_1(D,u1_struct_0(A)) & ? [E] : ( m1_subset_1(E,u1_struct_0(A)) & ! [F] : ( m1_subset_1(F,k1_numbers) => ! [G] : ( m1_subset_1(G,k1_numbers) => ! [H] : ( m1_subset_1(H,k1_numbers) => ! [I] : ( m1_subset_1(I,k1_numbers) => ( k4_rlvect_1(A,k4_rlvect_1(A,k4_rlvect_1(A,k3_rlvect_1(A,B,F),k3_rlvect_1(A,C,G)),k3_rlvect_1(A,D,H)),k3_rlvect_1(A,E,I)) = k1_rlvect_1(A) => ( F = 0 & G = 0 & H = 0 & I = 0 ) ) ) ) ) ) & ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ? [G] : ( m1_subset_1(G,k1_numbers) & ? [H] : ( m1_subset_1(H,k1_numbers) & ? [I] : ( m1_subset_1(I,k1_numbers) & ? [J] : ( m1_subset_1(J,k1_numbers) & F = k4_rlvect_1(A,k4_rlvect_1(A,k4_rlvect_1(A,k3_rlvect_1(A,B,G),k3_rlvect_1(A,C,H)),k3_rlvect_1(A,D,I)),k3_rlvect_1(A,E,J)) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l58_anproj_2,t22_anproj_2,d7_funcsdom,d3_rlvect_1,d3_rlvect_1,d3_rlvect_1,d4_rlvect_1,d4_rlvect_1,d4_rlvect_1,d4_rlvect_1,d2_rlvect_1,d4_rlvect_1,d3_rlvect_1,d3_rlvect_1,d3_rlvect_1,t2_anproj_2,d13_rlvect_1,d8_anproj_1]), [file(anproj_2,t23_anproj_2),interesting(0.00)]). fof(t27_anproj_2,theorem,( $true ), file(anproj_2,t27_anproj_2), [interesting(0.00)]). fof(d6_anproj_2,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ( v1_anproj_2(A) <=> ? [B] : ( m1_subset_1(B,u1_struct_0(A)) & ? [C] : ( m1_subset_1(C,u1_struct_0(A)) & ? [D] : ( m1_subset_1(D,u1_struct_0(A)) & ! [E] : ( m1_subset_1(E,k1_numbers) => ! [F] : ( m1_subset_1(F,k1_numbers) => ! [G] : ( m1_subset_1(G,k1_numbers) => ( k4_rlvect_1(A,k4_rlvect_1(A,k3_rlvect_1(A,B,E),k3_rlvect_1(A,C,F)),k3_rlvect_1(A,D,G)) = k1_rlvect_1(A) => ( E = 0 & F = 0 & G = 0 ) ) ) ) ) ) ) ) ) ) ), file(anproj_2,d6_anproj_2), [interesting(0.00)]). fof(l4_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,k1_numbers) => ! [F] : ( m1_subset_1(F,k1_numbers) => ! [G] : ( m1_subset_1(G,k1_numbers) => ! [H] : ( m1_subset_1(H,k1_numbers) => k3_rlvect_1(A,k4_rlvect_1(A,k4_rlvect_1(A,k3_rlvect_1(A,B,F),k3_rlvect_1(A,C,G)),k3_rlvect_1(A,D,H)),E) = k4_rlvect_1(A,k4_rlvect_1(A,k3_rlvect_1(A,B,k4_real_1(E,F)),k3_rlvect_1(A,C,k4_real_1(E,G))),k3_rlvect_1(A,D,k4_real_1(E,H))) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_rlvect_1,d9_rlvect_1,d9_rlvect_1,d9_rlvect_1,d9_rlvect_1]), [file(anproj_2,l4_anproj_2),interesting(0.00)]). fof(l5_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => k4_rlvect_1(A,k4_rlvect_1(A,k4_rlvect_1(A,B,C),D),k4_rlvect_1(A,k4_rlvect_1(A,E,F),G)) = k4_rlvect_1(A,k4_rlvect_1(A,k4_rlvect_1(A,B,E),k4_rlvect_1(A,C,F)),k4_rlvect_1(A,D,G)) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d6_rlvect_1,d6_rlvect_1,d6_rlvect_1,d6_rlvect_1,d6_rlvect_1,d6_rlvect_1]), [file(anproj_2,l5_anproj_2),interesting(0.00)]). fof(t15_anproj_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( ~ ( B != k1_rlvect_1(A) & C != k1_rlvect_1(A) & D != k1_rlvect_1(A) ) => r2_anproj_1(A,B,C,D) ) ) ) ) ) ), file(anproj_1,t15_anproj_1), [interesting(0.00)]). fof(t31_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( k5_rlvect_1(A,B) = k5_rlvect_1(A,C) => B = C ) ) ) ) ), file(rlvect_1,t31_rlvect_1), [interesting(0.00)]). fof(t30_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & ~ v3_realset2(A) & l2_rlvect_1(A) ) => ( ? [B] : ( m1_subset_1(B,u1_struct_0(k6_anproj_1(A))) & ? [C] : ( m1_subset_1(C,u1_struct_0(k6_anproj_1(A))) & B != C & ! [D] : ( m1_subset_1(D,u1_struct_0(k6_anproj_1(A))) => ! [E] : ( m1_subset_1(E,u1_struct_0(k6_anproj_1(A))) => ? [F] : ( m1_subset_1(F,u1_struct_0(k6_anproj_1(A))) & r1_collsp(k6_anproj_1(A),B,C,F) & r1_collsp(k6_anproj_1(A),D,E,F) ) ) ) ) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(k6_anproj_1(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k6_anproj_1(A))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k6_anproj_1(A))) => ! [E] : ( m1_subset_1(E,u1_struct_0(k6_anproj_1(A))) => ? [F] : ( m1_subset_1(F,u1_struct_0(k6_anproj_1(A))) & r1_collsp(k6_anproj_1(A),B,C,F) & r1_collsp(k6_anproj_1(A),D,E,F) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d8_anproj_2,t25_anproj_2,d9_anproj_2,d8_anproj_2,t25_anproj_2,d9_anproj_2,d8_anproj_2,t25_anproj_2,d9_anproj_2,d8_anproj_2,t25_anproj_2,d9_anproj_2,d7_anproj_2,d7_anproj_2,d7_anproj_2,t25_anproj_2,d8_anproj_2,d7_anproj_2,t25_anproj_2,d8_anproj_2,d7_anproj_2,t25_anproj_2,d8_anproj_2,d7_anproj_2,t25_anproj_2,d8_anproj_2,d7_anproj_2,t25_anproj_2,d8_anproj_2,d7_anproj_2,t25_anproj_2,d8_anproj_2,d7_anproj_2,t25_anproj_2,d8_anproj_2,d7_anproj_2,t25_anproj_2,d8_anproj_2]), [file(anproj_2,t30_anproj_2),interesting(0.00)]). fof(d14_anproj_2,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v2_collsp(A) & v3_collsp(A) & v4_collsp(A) & v2_anproj_2(A) & v3_anproj_2(A) & l1_collsp(A) ) => ( v7_anproj_2(A) <=> ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ? [F] : ( m1_subset_1(F,u1_struct_0(A)) & r1_collsp(A,B,C,F) & r1_collsp(A,D,E,F) ) ) ) ) ) ) ) ), file(anproj_2,d14_anproj_2), [interesting(0.00)]). fof(t31_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & ~ v3_realset2(A) & l2_rlvect_1(A) ) => ~ ( ? [B] : ( m1_subset_1(B,u1_struct_0(A)) & ? [C] : ( m1_subset_1(C,u1_struct_0(A)) & ? [D] : ( m1_subset_1(D,u1_struct_0(A)) & ! [E] : ( m1_subset_1(E,k1_numbers) => ! [F] : ( m1_subset_1(F,k1_numbers) => ! [G] : ( m1_subset_1(G,k1_numbers) => ( k4_rlvect_1(A,k4_rlvect_1(A,k3_rlvect_1(A,B,E),k3_rlvect_1(A,C,F)),k3_rlvect_1(A,D,G)) = k1_rlvect_1(A) => ( E = 0 & F = 0 & G = 0 ) ) ) ) ) & ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ? [F] : ( m1_subset_1(F,k1_numbers) & ? [G] : ( m1_subset_1(G,k1_numbers) & ? [H] : ( m1_subset_1(H,k1_numbers) & E = k4_rlvect_1(A,k4_rlvect_1(A,k3_rlvect_1(A,B,F),k3_rlvect_1(A,C,G)),k3_rlvect_1(A,D,H)) ) ) ) ) ) ) ) & ! [B] : ( ( ~ v3_struct_0(B) & v2_collsp(B) & v3_collsp(B) & v4_collsp(B) & v2_anproj_2(B) & v3_anproj_2(B) & l1_collsp(B) ) => ~ ( B = k6_anproj_1(A) & v7_anproj_2(B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d6_anproj_2,t29_anproj_2,t30_anproj_2,d14_anproj_2]), [file(anproj_2,t31_anproj_2),interesting(0.00)]). fof(l89_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & ~ v3_realset2(A) & l2_rlvect_1(A) ) => ( ? [B] : ( m1_subset_1(B,u1_struct_0(A)) & ? [C] : ( m1_subset_1(C,u1_struct_0(A)) & ? [D] : ( m1_subset_1(D,u1_struct_0(A)) & ? [E] : ( m1_subset_1(E,u1_struct_0(A)) & ! [F] : ( m1_subset_1(F,k1_numbers) => ! [G] : ( m1_subset_1(G,k1_numbers) => ! [H] : ( m1_subset_1(H,k1_numbers) => ! [I] : ( m1_subset_1(I,k1_numbers) => ( k4_rlvect_1(A,k4_rlvect_1(A,k4_rlvect_1(A,k3_rlvect_1(A,B,F),k3_rlvect_1(A,C,G)),k3_rlvect_1(A,D,H)),k3_rlvect_1(A,E,I)) = k1_rlvect_1(A) => ( F = 0 & G = 0 & H = 0 & I = 0 ) ) ) ) ) ) ) ) ) ) => v1_anproj_2(A) ) ) ), inference(mizar_proof,[status(thm)],[d6_anproj_2,t10_rlvect_1,t23_rlvect_1]), [file(anproj_2,l89_anproj_2),interesting(0.00)]). fof(l75_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & v1_anproj_2(A) & l2_rlvect_1(A) ) => ( ~ v3_struct_0(k6_anproj_1(A)) & v2_collsp(k6_anproj_1(A)) & v3_collsp(k6_anproj_1(A)) & v4_collsp(k6_anproj_1(A)) & v2_anproj_2(k6_anproj_1(A)) & v3_anproj_2(k6_anproj_1(A)) & l1_collsp(k6_anproj_1(A)) ) ) ), file(anproj_2,l75_anproj_2), [interesting(0.00)]). fof(t28_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k6_rlvect_1(A,B,B) = k1_rlvect_1(A) ) ) ), file(rlvect_1,t28_rlvect_1), [interesting(0.00)]). fof(d6_collsp,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_collsp(A) ) => ( v4_collsp(A) <=> ~ ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => r1_collsp(A,B,C,D) ) ) ) ) ) ), file(collsp,d6_collsp), [interesting(0.00)]). fof(d10_anproj_2,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_collsp(A) ) => ( v3_anproj_2(A) <=> ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ? [D] : ( m1_subset_1(D,u1_struct_0(A)) & B != D & C != D & r1_collsp(A,B,C,D) ) ) ) ) ) ), file(anproj_2,d10_anproj_2), [interesting(0.00)]). fof(t21_anproj_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( ( v8_rlvect_1(B,A) & v8_rlvect_1(C,A) ) => ( r1_anproj_1(A,B,C) | ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ? [F] : ( m1_subset_1(F,u1_struct_0(A)) & v8_rlvect_1(F,A) & r2_anproj_1(A,D,E,F) & ~ r1_anproj_1(A,D,F) & ~ r1_anproj_1(A,E,F) ) ) ) ) ) ) ) ) ), file(anproj_1,t21_anproj_1), [interesting(0.00)]). fof(l7_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,k1_numbers) => ! [G] : ( m1_subset_1(G,k1_numbers) => ! [H] : ( m1_subset_1(H,k1_numbers) => ! [I] : ( m1_subset_1(I,k1_numbers) => ! [J] : ( m1_subset_1(J,k1_numbers) => k3_rlvect_1(A,k4_rlvect_1(A,k4_rlvect_1(A,k4_rlvect_1(A,k3_rlvect_1(A,B,G),k3_rlvect_1(A,C,H)),k3_rlvect_1(A,D,I)),k3_rlvect_1(A,E,J)),F) = k4_rlvect_1(A,k4_rlvect_1(A,k4_rlvect_1(A,k3_rlvect_1(A,B,k4_real_1(F,G)),k3_rlvect_1(A,C,k4_real_1(F,H))),k3_rlvect_1(A,D,k4_real_1(F,I))),k3_rlvect_1(A,E,k4_real_1(F,J))) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_rlvect_1,d9_rlvect_1,d9_rlvect_1,d9_rlvect_1,d9_rlvect_1,d9_rlvect_1,d9_rlvect_1]), [file(anproj_2,l7_anproj_2),interesting(0.00)]). fof(l8_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ! [H] : ( m1_subset_1(H,u1_struct_0(A)) => ! [I] : ( m1_subset_1(I,u1_struct_0(A)) => k4_rlvect_1(A,k4_rlvect_1(A,k4_rlvect_1(A,k4_rlvect_1(A,B,C),D),E),k4_rlvect_1(A,k4_rlvect_1(A,k4_rlvect_1(A,F,G),H),I)) = k4_rlvect_1(A,k4_rlvect_1(A,k4_rlvect_1(A,k4_rlvect_1(A,B,F),k4_rlvect_1(A,C,G)),k4_rlvect_1(A,D,H)),k4_rlvect_1(A,E,I)) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d6_rlvect_1,d6_rlvect_1,d6_rlvect_1,d6_rlvect_1,d6_rlvect_1,d6_rlvect_1,d6_rlvect_1,d6_rlvect_1,d6_rlvect_1]), [file(anproj_2,l8_anproj_2),interesting(0.00)]). fof(l9_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,k1_numbers) => ! [F] : ( m1_subset_1(F,k1_numbers) => ! [G] : ( m1_subset_1(G,k1_numbers) => ! [H] : ( m1_subset_1(H,k1_numbers) => k3_rlvect_1(A,k4_rlvect_1(A,k4_rlvect_1(A,k3_rlvect_1(A,B,F),k3_rlvect_1(A,C,G)),k3_rlvect_1(A,D,H)),E) = k4_rlvect_1(A,k4_rlvect_1(A,k3_rlvect_1(A,B,k4_real_1(E,F)),k3_rlvect_1(A,C,k4_real_1(E,G))),k3_rlvect_1(A,D,k4_real_1(E,H))) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_rlvect_1,d9_rlvect_1,d9_rlvect_1,d9_rlvect_1,d9_rlvect_1]), [file(anproj_2,l9_anproj_2),interesting(0.00)]). fof(l10_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,k1_numbers) => ! [H] : ( m1_subset_1(H,k1_numbers) => ! [I] : ( m1_subset_1(I,k1_numbers) => ! [J] : ( m1_subset_1(J,k1_numbers) => ! [K] : ( m1_subset_1(K,k1_numbers) => ( ( B = k4_rlvect_1(A,k3_rlvect_1(A,C,G),k3_rlvect_1(A,D,H)) & D = k4_rlvect_1(A,k4_rlvect_1(A,k3_rlvect_1(A,C,I),k3_rlvect_1(A,E,J)),k3_rlvect_1(A,F,K)) ) => B = k4_rlvect_1(A,k4_rlvect_1(A,k3_rlvect_1(A,C,k3_real_1(G,k4_real_1(H,I))),k3_rlvect_1(A,E,k4_real_1(H,J))),k3_rlvect_1(A,F,k4_real_1(H,K))) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l9_anproj_2,d6_rlvect_1,d6_rlvect_1,d9_rlvect_1,d6_rlvect_1]), [file(anproj_2,l10_anproj_2),interesting(0.00)]). fof(l92_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & ~ v3_realset2(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(k6_anproj_1(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k6_anproj_1(A))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k6_anproj_1(A))) => ! [E] : ( m1_subset_1(E,u1_struct_0(k6_anproj_1(A))) => ! [F] : ( m1_subset_1(F,u1_struct_0(k6_anproj_1(A))) => ! [G] : ( m1_subset_1(G,u1_struct_0(k6_anproj_1(A))) => ~ ( ~ r1_collsp(k6_anproj_1(A),G,D,C) & r1_collsp(k6_anproj_1(A),D,C,B) & r1_collsp(k6_anproj_1(A),G,E,D) & r1_collsp(k6_anproj_1(A),G,F,C) & ! [H] : ( m1_subset_1(H,u1_struct_0(k6_anproj_1(A))) => ~ ( r1_collsp(k6_anproj_1(A),E,F,H) & r1_collsp(k6_anproj_1(A),G,B,H) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d7_anproj_2,t25_anproj_2,t25_anproj_2,t25_anproj_2,d9_anproj_2,t25_anproj_2,d9_anproj_2,d7_anproj_2,d8_anproj_2,t25_anproj_2,d9_anproj_2,t25_anproj_2,d7_anproj_2,d8_anproj_2,t25_anproj_2,d7_anproj_2,d8_anproj_2,t25_anproj_2]), [file(anproj_2,l92_anproj_2),interesting(0.00)]). fof(t19_collsp,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_collsp(A) & v3_collsp(A) & v4_collsp(A) & l1_collsp(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ~ ( B != C & ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => r1_collsp(A,B,C,D) ) ) ) ) ) ), file(collsp,t19_collsp), [interesting(0.00)]). fof(d15_anproj_2,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v2_collsp(A) & v3_collsp(A) & v4_collsp(A) & v2_anproj_2(A) & v3_anproj_2(A) & l1_collsp(A) ) => ( v8_anproj_2(A) <=> ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ? [G] : ( m1_subset_1(G,u1_struct_0(A)) & ? [H] : ( m1_subset_1(H,u1_struct_0(A)) & r1_collsp(A,B,D,G) & r1_collsp(A,C,E,H) & r1_collsp(A,F,G,H) ) ) ) ) ) ) ) ) ) ), file(anproj_2,d15_anproj_2), [interesting(0.00)]). fof(t37_anproj_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_collsp(A) ) => ( ( ~ v3_struct_0(A) & v2_collsp(A) & v3_collsp(A) & v4_collsp(A) & v2_anproj_2(A) & v3_anproj_2(A) & v7_anproj_2(A) & l1_collsp(A) ) <=> ( ~ v3_struct_0(A) & v2_collsp(A) & v3_collsp(A) & v4_collsp(A) & v3_anproj_2(A) & l1_collsp(A) & ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ? [F] : ( m1_subset_1(F,u1_struct_0(A)) & r1_collsp(A,B,C,F) & r1_collsp(A,D,E,F) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d14_anproj_2,d9_anproj_2,d14_anproj_2]), [file(anproj_2,t37_anproj_2),interesting(0.00)]).