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) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t17_anproj_1,t11_anproj_1,t11_anproj_1,l29_anproj_1,l29_anproj_1,d6_rlvect_1,d6_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,t23_rlvect_1,d9_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_1,t20_anproj_1),interesting(1.00)]). fof(l32_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) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ~ ( v8_rlvect_1(E,A) & v8_rlvect_1(F,A) & ~ r1_anproj_1(A,E,F) & ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => r2_anproj_1(A,E,F,G) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t19_anproj_1]), [file(anproj_1,l32_anproj_1),interesting(0.87)]). 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) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t11_anproj_1,t11_anproj_1,t11_anproj_1,t23_rlvect_1,t23_rlvect_1,t10_rlvect_1,l17_anproj_1,l17_anproj_1,l18_anproj_1,l19_anproj_1,t16_anproj_1,t16_anproj_1,t15_anproj_1,t15_anproj_1,t15_anproj_1,t14_anproj_1,d3_anproj_1]), [file(anproj_1,t19_anproj_1),interesting(0.86)]). fof(t22_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) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ~ ( v8_rlvect_1(E,A) & v8_rlvect_1(F,A) & ~ r1_anproj_1(A,E,F) & ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ~ ( v8_rlvect_1(G,A) & ~ r2_anproj_1(A,E,F,G) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l32_anproj_1,t17_anproj_1]), [file(anproj_1,t22_anproj_1),interesting(0.81)]). 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) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_anproj_1,t16_rlvect_1,t29_rlvect_1,d9_rlvect_1,t23_rlvect_1,t10_rlvect_1,d3_anproj_1,t10_anproj_1,t10_anproj_1]), [file(anproj_1,t16_anproj_1),interesting(0.80)]). 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) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_anproj_1,d2_anproj_1,d9_rlvect_1,d9_rlvect_1,d7_xcmplx_0,d9_rlvect_1,d9_rlvect_1,t203_xcmplx_1,t6_xcmplx_1,t6_xcmplx_1,d2_anproj_1]), [file(anproj_1,t6_anproj_1),interesting(0.76)]). 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) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d13_rlvect_1,t18_anproj_1,d13_rlvect_1,d13_rlvect_1,d9_rlvect_1,d9_rlvect_1,t29_rlvect_1,t45_rlvect_1,d6_rlvect_1,d6_rlvect_1,t16_rlvect_1,t10_rlvect_1,t16_rlvect_1,d3_anproj_1,d9_rlvect_1,d6_rlvect_1,t16_rlvect_1,t10_rlvect_1,t39_rlvect_1,t38_rlvect_1,d9_rlvect_1,t23_rlvect_1,t24_rlvect_1,d2_anproj_1,d2_anproj_1,d9_rlvect_1,d6_rlvect_1,t16_rlvect_1,t10_rlvect_1,t39_rlvect_1,t38_rlvect_1,d9_rlvect_1,t23_rlvect_1,t24_rlvect_1,d2_anproj_1,d2_anproj_1,t6_anproj_1,t16_anproj_1,t6_anproj_1,t16_anproj_1,t6_anproj_1,d13_rlvect_1,t7_anproj_1,t15_anproj_1,t7_anproj_1,t15_anproj_1,t6_anproj_1,d13_rlvect_1,t7_anproj_1,t15_anproj_1,t7_anproj_1,t15_anproj_1,t6_anproj_1]), [file(anproj_1,t21_anproj_1),interesting(0.76)]). 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) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t17_anproj_1,t17_anproj_1,t11_anproj_1,t11_anproj_1,t11_anproj_1,t11_anproj_1,t11_anproj_1,t11_anproj_1,d3_anproj_1,l34_anproj_1,d3_anproj_1,l34_anproj_1,d3_anproj_1,l34_anproj_1,d3_anproj_1,d6_rlvect_1,l34_anproj_1,d3_anproj_1,t6_xcmplx_1,t6_xcmplx_1,t23_rlvect_1,t23_rlvect_1,t10_rlvect_1,d13_rlvect_1,t6_xcmplx_1,t6_xcmplx_1,t23_rlvect_1,t23_rlvect_1,t10_rlvect_1,d13_rlvect_1,t6_xcmplx_1,t6_xcmplx_1,t23_rlvect_1,t23_rlvect_1,t10_rlvect_1,d13_rlvect_1]), [file(anproj_1,t23_anproj_1),interesting(0.74)]). 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) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t15_anproj_1,d13_rlvect_1,t16_anproj_1]), [file(anproj_1,t17_anproj_1),interesting(0.72)]). fof(t7_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)) => ( r1_anproj_1(A,B,k1_rlvect_1(A)) <=> B = k1_rlvect_1(A) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_anproj_1,t23_rlvect_1,t24_rlvect_1]), [file(anproj_1,t7_anproj_1),interesting(0.72)]). fof(t18_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)) => ( k4_rlvect_1(A,B,C) = k1_rlvect_1(A) => r1_anproj_1(A,B,C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d10_rlvect_1,t29_rlvect_1,t5_anproj_1]), [file(anproj_1,t18_anproj_1),interesting(0.68)]). 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)) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d13_rlvect_1,t10_anproj_1,d3_anproj_1,t23_rlvect_1,t10_rlvect_1,l14_anproj_1,d2_anproj_1,t23_rlvect_1,t10_rlvect_1,t24_rlvect_1,t23_rlvect_1,t10_rlvect_1,t24_rlvect_1,l15_anproj_1,t16_rlvect_1,t29_rlvect_1,d3_anproj_1]), [file(anproj_1,t11_anproj_1),interesting(0.57)]). fof(t26_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)) => ( r2_hidden(B,k1_anproj_1(A)) <=> v8_rlvect_1(B,A) ) ) ) ), inference(mizar_proof,[status(thm)],[d4_anproj_1,d13_rlvect_1,d13_rlvect_1,d4_anproj_1]), [file(anproj_1,t26_anproj_1),interesting(0.56)]). fof(t34_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)) => ( v8_rlvect_1(B,A) => m1_subset_1(k3_anproj_1(A,B),k4_anproj_1(A)) ) ) ) ), inference(mizar_proof,[status(thm)],[t26_anproj_1,d5_eqrel_1,d7_anproj_1]), [file(anproj_1,t34_anproj_1),interesting(0.56)]). 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) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_anproj_1,d9_rlvect_1,d7_xcmplx_0,d9_rlvect_1,d9_rlvect_1,t203_xcmplx_1,t6_xcmplx_1,d9_rlvect_1,d2_anproj_1]), [file(anproj_1,t5_anproj_1),interesting(0.51)]). 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) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t26_anproj_1,t44_eqrel_1,t29_anproj_1,t29_anproj_1,t44_eqrel_1]), [file(anproj_1,t35_anproj_1),interesting(0.51)]). fof(t29_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)) => ( r2_hidden(k4_tarski(B,C),k2_anproj_1(A)) <=> ( v8_rlvect_1(B,A) & v8_rlvect_1(C,A) & r1_anproj_1(A,B,C) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d5_anproj_1,d5_anproj_1,t26_anproj_1,t26_anproj_1,d5_anproj_1]), [file(anproj_1,t29_anproj_1),interesting(0.47)]). fof(l17_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,k1_numbers) => ! [D] : ( m1_subset_1(D,k1_numbers) => ! [E] : ( m1_subset_1(E,k1_numbers) => k3_rlvect_1(A,B,k3_real_1(k3_real_1(C,D),E)) = k4_rlvect_1(A,k4_rlvect_1(A,k3_rlvect_1(A,B,C),k3_rlvect_1(A,B,D)),k3_rlvect_1(A,B,E)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_rlvect_1,d9_rlvect_1]), [file(anproj_1,l17_anproj_1),interesting(0.46)]). fof(l21_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) => ( k4_rlvect_1(A,B,k3_rlvect_1(A,C,E)) = k4_rlvect_1(A,D,k3_rlvect_1(A,C,F)) => k4_rlvect_1(A,k3_rlvect_1(A,C,k5_real_1(E,F)),B) = D ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d6_rlvect_1,t16_rlvect_1,t10_rlvect_1,d6_rlvect_1,d11_rlvect_1,t49_rlvect_1]), [file(anproj_1,l21_anproj_1),interesting(0.45)]). fof(t28_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,C] : ( r2_hidden(k4_tarski(B,C),k2_anproj_1(A)) => ( m1_subset_1(B,u1_struct_0(A)) & m1_subset_1(C,u1_struct_0(A)) ) ) ) ), inference(mizar_proof,[status(thm)],[d5_anproj_1]), [file(anproj_1,t28_anproj_1),interesting(0.44)]). fof(l29_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,k1_numbers) => ! [E] : ( m1_subset_1(E,k1_numbers) => ! [F] : ( m1_subset_1(F,k1_numbers) => k3_rlvect_1(A,k4_rlvect_1(A,k3_rlvect_1(A,B,E),k3_rlvect_1(A,C,F)),D) = k4_rlvect_1(A,k3_rlvect_1(A,B,k4_real_1(D,E)),k3_rlvect_1(A,C,k4_real_1(D,F))) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_rlvect_1,d9_rlvect_1,d9_rlvect_1]), [file(anproj_1,l29_anproj_1),interesting(0.43)]). fof(l19_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,k1_numbers) => ! [E] : ( m1_subset_1(E,k1_numbers) => ! [F] : ( m1_subset_1(F,k1_numbers) => k4_rlvect_1(A,k3_rlvect_1(A,B,k4_real_1(D,E)),k3_rlvect_1(A,C,k4_real_1(D,F))) = k3_rlvect_1(A,k4_rlvect_1(A,k3_rlvect_1(A,B,E),k3_rlvect_1(A,C,F)),D) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_rlvect_1,d9_rlvect_1,d9_rlvect_1]), [file(anproj_1,l19_anproj_1),interesting(0.43)]). fof(l14_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,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) => k3_rlvect_1(A,B,D) = k3_rlvect_1(A,C,k1_real_1(E)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t19_rlvect_1,t39_rlvect_1,t38_rlvect_1]), [file(anproj_1,l14_anproj_1),interesting(0.38)]). 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) ) ) ) ), inference(mizar_proof,[status(thm)],[d7_anproj_1,d3_tarski,d5_eqrel_1,d4_anproj_1,d4_anproj_1,d13_rlvect_1,t34_anproj_1]), [file(anproj_1,t42_anproj_1),interesting(0.34)]). fof(t12_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,k1_numbers) => ! [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,k3_rlvect_1(A,B,D),k3_rlvect_1(A,C,E)) = k4_rlvect_1(A,k3_rlvect_1(A,B,F),k3_rlvect_1(A,C,G)) & v8_rlvect_1(B,A) & v8_rlvect_1(C,A) ) => ( r1_anproj_1(A,B,C) | ( D = F & E = G ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d13_rlvect_1,d6_rlvect_1,t16_rlvect_1,t10_rlvect_1,d6_rlvect_1,d11_rlvect_1,t49_rlvect_1,d6_rlvect_1,t16_rlvect_1,t10_rlvect_1,d11_rlvect_1,t49_rlvect_1,t23_rlvect_1,t24_rlvect_1,t23_rlvect_1,t24_rlvect_1,d2_anproj_1]), [file(anproj_1,t12_anproj_1),interesting(0.23)]). 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 ) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l21_anproj_1,d6_rlvect_1,l21_anproj_1,d6_rlvect_1,t10_rlvect_1,l21_anproj_1,d6_rlvect_1,d3_anproj_1]), [file(anproj_1,t13_anproj_1),interesting(0.19)]). 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) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_anproj_1,t35_anproj_1,t9_anproj_1,d9_anproj_1]), [file(anproj_1,t41_anproj_1),interesting(0.17)]). fof(l15_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) => ( 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 | B = k4_rlvect_1(A,k3_rlvect_1(A,C,k1_real_1(k4_real_1(k2_real_1(E),F))),k3_rlvect_1(A,D,k1_real_1(k4_real_1(k2_real_1(E),G)))) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d6_rlvect_1,t19_rlvect_1,t45_rlvect_1,t39_rlvect_1,t39_rlvect_1,t38_rlvect_1,t38_rlvect_1,t12_analoaf,d9_rlvect_1,d9_rlvect_1,d9_rlvect_1]), [file(anproj_1,l15_anproj_1),interesting(0.15)]). fof(l34_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) => ! [K] : ( m1_subset_1(K,k1_numbers) => ! [L] : ( m1_subset_1(L,k1_numbers) => ! [M] : ( m1_subset_1(M,k1_numbers) => k4_rlvect_1(A,k4_rlvect_1(A,k3_rlvect_1(A,k4_rlvect_1(A,k3_rlvect_1(A,B,E),k3_rlvect_1(A,C,F)),K),k3_rlvect_1(A,k4_rlvect_1(A,k3_rlvect_1(A,C,G),k3_rlvect_1(A,D,H)),L)),k3_rlvect_1(A,k4_rlvect_1(A,k3_rlvect_1(A,B,I),k3_rlvect_1(A,D,J)),M)) = k4_rlvect_1(A,k4_rlvect_1(A,k3_rlvect_1(A,B,k3_real_1(k4_real_1(K,E),k4_real_1(M,I))),k3_rlvect_1(A,C,k3_real_1(k4_real_1(K,F),k4_real_1(L,G)))),k3_rlvect_1(A,D,k3_real_1(k4_real_1(L,H),k4_real_1(M,J)))) ) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l29_anproj_1,d6_rlvect_1,d6_rlvect_1,d9_rlvect_1,d6_rlvect_1,d6_rlvect_1,d9_rlvect_1,d6_rlvect_1,d6_rlvect_1,d6_rlvect_1,d9_rlvect_1,d6_rlvect_1]), [file(anproj_1,l34_anproj_1),interesting(0.13)]). 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(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(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(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(t49_rlvect_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( ( ~ v3_struct_0(C) & v3_rlvect_1(C) & v4_rlvect_1(C) & v5_rlvect_1(C) & v6_rlvect_1(C) & v7_rlvect_1(C) & l2_rlvect_1(C) ) => ! [D] : ( m1_subset_1(D,u1_struct_0(C)) => k3_rlvect_1(C,D,k5_real_1(A,B)) = k6_rlvect_1(C,k3_rlvect_1(C,D,A),k3_rlvect_1(C,D,B)) ) ) ) ) ), file(rlvect_1,t49_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(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(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(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(t1_anproj_1,theorem,( $true ), file(anproj_1,t1_anproj_1), [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) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_anproj_1,d6_rlvect_1,d6_rlvect_1,d3_anproj_1]), [file(anproj_1,t10_anproj_1),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) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t10_rlvect_1,t23_rlvect_1,t23_rlvect_1,t10_rlvect_1,t23_rlvect_1,d3_anproj_1,t10_anproj_1,t10_anproj_1]), [file(anproj_1,t15_anproj_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(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(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(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(t12_analoaf,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 | B = k3_rlvect_1(A,C,k2_real_1(D)) ) ) ) ) ) ) ), file(analoaf,t12_analoaf), [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(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(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(l18_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)) => 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_1,l18_anproj_1),interesting(0.00)]). fof(t14_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,k1_numbers) => ! [G] : ( m1_subset_1(G,k1_numbers) => ! [H] : ( m1_subset_1(H,k1_numbers) => ! [I] : ( m1_subset_1(I,k1_numbers) => ~ ( ~ r1_anproj_1(A,B,C) & D = k4_rlvect_1(A,k3_rlvect_1(A,B,F),k3_rlvect_1(A,C,G)) & E = k4_rlvect_1(A,k3_rlvect_1(A,B,H),k3_rlvect_1(A,C,I)) & k5_real_1(k4_real_1(F,I),k4_real_1(H,G)) = 0 & v8_rlvect_1(B,A) & v8_rlvect_1(C,A) & ~ r1_anproj_1(A,D,E) & D != k1_rlvect_1(A) & E != k1_rlvect_1(A) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t6_xcmplx_1,t23_rlvect_1,t23_rlvect_1,t10_rlvect_1,t203_xcmplx_1,t23_rlvect_1,t10_rlvect_1,t12_analoaf,d9_rlvect_1,d9_rlvect_1,t6_xcmplx_1,t23_rlvect_1,t23_rlvect_1,t10_rlvect_1,d2_anproj_1,t6_xcmplx_1,t23_rlvect_1,t10_rlvect_1,t203_xcmplx_1,t12_analoaf,d9_rlvect_1,d9_rlvect_1,t6_xcmplx_1,d2_anproj_1,l19_anproj_1,t6_xcmplx_1,d2_anproj_1]), [file(anproj_1,t14_anproj_1),interesting(0.00)]). fof(t24_anproj_1,theorem,( $true ), file(anproj_1,t24_anproj_1), [interesting(0.00)]). fof(t25_anproj_1,theorem,( $true ), file(anproj_1,t25_anproj_1), [interesting(0.00)]). fof(t27_anproj_1,theorem,( $true ), file(anproj_1,t27_anproj_1), [interesting(0.00)]). fof(d5_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] : ( ( v3_relat_2(B) & v8_relat_2(B) & v1_partfun1(B,k1_anproj_1(A),k1_anproj_1(A)) & m2_relset_1(B,k1_anproj_1(A),k1_anproj_1(A)) ) => ( B = k2_anproj_1(A) <=> ! [C,D] : ( r2_hidden(k4_tarski(C,D),B) <=> ( r2_hidden(C,k1_anproj_1(A)) & r2_hidden(D,k1_anproj_1(A)) & ? [E] : ( m1_subset_1(E,u1_struct_0(A)) & ? [F] : ( m1_subset_1(F,u1_struct_0(A)) & C = E & D = F & r1_anproj_1(A,E,F) ) ) ) ) ) ) ) ), file(anproj_1,d5_anproj_1), [interesting(0.00)]). fof(t2_anproj_1,theorem,( $true ), file(anproj_1,t2_anproj_1), [interesting(0.00)]). fof(t30_anproj_1,theorem,( $true ), file(anproj_1,t30_anproj_1), [interesting(0.00)]). fof(t31_anproj_1,theorem,( $true ), file(anproj_1,t31_anproj_1), [interesting(0.00)]). fof(t32_anproj_1,theorem,( $true ), file(anproj_1,t32_anproj_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(d4_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] : ( B = k1_anproj_1(A) <=> ! [C] : ( r2_hidden(C,B) <=> ( C != k1_rlvect_1(A) & m1_subset_1(C,u1_struct_0(A)) ) ) ) ) ), file(anproj_1,d4_anproj_1), [interesting(0.00)]). fof(t33_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) ) => ( ( ~ 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)) & r2_hidden(B,k1_anproj_1(A)) ) ) ) ), inference(mizar_proof,[status(thm)],[d8_anproj_1,t26_anproj_1,d13_rlvect_1,d4_anproj_1,d8_anproj_1]), [file(anproj_1,t33_anproj_1),interesting(0.00)]). fof(t36_anproj_1,theorem,( $true ), file(anproj_1,t36_anproj_1), [interesting(0.00)]). fof(t37_anproj_1,theorem,( $true ), file(anproj_1,t37_anproj_1), [interesting(0.00)]). fof(t38_anproj_1,theorem,( $true ), file(anproj_1,t38_anproj_1), [interesting(0.00)]). fof(t39_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) ) => ( u1_struct_0(k6_anproj_1(A)) = k4_anproj_1(A) & u1_collsp(k6_anproj_1(A)) = k5_anproj_1(A) ) ) ), file(anproj_1,t39_anproj_1), [interesting(0.00)]). fof(t3_anproj_1,theorem,( $true ), file(anproj_1,t3_anproj_1), [interesting(0.00)]). fof(d9_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) & ~ v3_realset2(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_collsp(B,k4_anproj_1(A)) => ( B = k5_anproj_1(A) <=> ! [C,D,E] : ( r2_hidden(k3_mcart_1(C,D,E),B) <=> ? [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)) & C = k3_anproj_1(A,F) & D = k3_anproj_1(A,G) & E = k3_anproj_1(A,H) & v8_rlvect_1(F,A) & v8_rlvect_1(G,A) & v8_rlvect_1(H,A) & r2_anproj_1(A,F,G,H) ) ) ) ) ) ) ) ), file(anproj_1,d9_anproj_1), [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) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_anproj_1]), [file(anproj_1,t40_anproj_1),interesting(0.00)]). fof(t44_eqrel_1,theorem,( ! [A,B,C] : ( ( v3_relat_2(C) & v8_relat_2(C) & v1_partfun1(C,A,A) & m2_relset_1(C,A,A) ) => ! [D] : ( r2_hidden(D,A) => ( r2_hidden(k4_tarski(D,B),C) <=> k6_eqrel_1(A,C,D) = k6_eqrel_1(A,C,B) ) ) ) ), file(eqrel_1,t44_eqrel_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) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t5_anproj_1,t5_anproj_1,t5_anproj_1,d3_anproj_1,d9_rlvect_1,d9_rlvect_1,d9_rlvect_1,t6_xcmplx_1,d3_anproj_1]), [file(anproj_1,t9_anproj_1),interesting(0.00)]). fof(d7_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] : ( B = k4_anproj_1(A) <=> ? [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_zfmisc_1(k1_anproj_1(A)))) & C = k8_eqrel_1(k1_anproj_1(A),k2_anproj_1(A)) & B = C ) ) ) ), file(anproj_1,d7_anproj_1), [interesting(0.00)]). fof(d3_tarski,definition,( ! [A,B] : ( r1_tarski(A,B) <=> ! [C] : ( r2_hidden(C,A) => r2_hidden(C,B) ) ) ), file(tarski,d3_tarski), [interesting(0.00)]). fof(d5_eqrel_1,definition,( ! [A,B] : ( ( v3_relat_2(B) & v8_relat_2(B) & v1_partfun1(B,A,A) & m2_relset_1(B,A,A) ) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_zfmisc_1(A))) => ( C = k7_eqrel_1(A,B) <=> ! [D] : ( m1_subset_1(D,k1_zfmisc_1(A)) => ( r2_hidden(D,C) <=> ? [E] : ( r2_hidden(E,A) & D = k6_eqrel_1(A,B,E) ) ) ) ) ) ) ), file(eqrel_1,d5_eqrel_1), [interesting(0.00)]). fof(t4_anproj_1,theorem,( $true ), file(anproj_1,t4_anproj_1), [interesting(0.00)]). fof(t8_anproj_1,theorem,( $true ), file(anproj_1,t8_anproj_1), [interesting(0.00)]).