% Mizar problem: t14_projred1,projred1,185,34 fof(t14_projred1,conjecture,( ! [A] : ( ( v1_incproj(A) & v2_incproj(A) & v3_incproj(A) & v4_incproj(A) & v5_incproj(A) & v10_incproj(A) & l1_incsp_1(A) ) => ! [B] : ( m1_subset_1(B,u1_incsp_1(A)) => ! [C] : ( m1_subset_1(C,u1_incsp_1(A)) => ! [D] : ( m1_subset_1(D,u1_incsp_1(A)) => ! [E] : ( m1_subset_1(E,u1_incsp_1(A)) => ! [F] : ( m1_subset_1(F,u1_incsp_1(A)) => ! [G] : ( m1_subset_1(G,u1_incsp_1(A)) => ! [H] : ( m1_subset_1(H,u1_incsp_1(A)) => ! [I] : ( m1_subset_1(I,u1_incsp_1(A)) => ! [J] : ( m1_subset_1(J,u1_incsp_1(A)) => ! [K] : ( m1_subset_1(K,u1_incsp_1(A)) => ! [L] : ( m1_subset_1(L,u2_incsp_1(A)) => ! [M] : ( m1_subset_1(M,u2_incsp_1(A)) => ! [N] : ( m1_subset_1(N,u2_incsp_1(A)) => ! [O] : ( m1_subset_1(O,u2_incsp_1(A)) => ! [P] : ( m1_subset_1(P,u2_incsp_1(A)) => ! [Q] : ( m1_subset_1(Q,u2_incsp_1(A)) => ! [R] : ( m1_subset_1(R,u2_incsp_1(A)) => ! [S] : ( m1_subset_1(S,u2_incsp_1(A)) => ! [T] : ( m1_subset_1(T,u2_incsp_1(A)) => ~ ( r4_incproj(A,B,C,L,D) & r4_incproj(A,B,F,M,E) & r4_incproj(A,B,H,N,G) & r4_incproj(A,H,F,O,K) & r4_incproj(A,H,I,P,D) & r4_incproj(A,F,J,Q,D) & r4_incproj(A,K,E,R,G) & r4_incproj(A,C,I,S,G) & r4_incproj(A,C,J,T,E) & r1_incproj(L,M,N) & B != H & B != C & B != E & F != E & ! [U] : ( m1_subset_1(U,u2_incsp_1(A)) => ~ r4_incproj(A,I,J,U,K) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_bg_added,[status(thm)],[antisymmetry_r2_hidden,cc1_funct_1,d10_incproj,d19_incproj,d5_incproj,d8_incproj,d9_incproj,dt_k1_xboole_0,dt_l1_incsp_1,dt_m1_subset_1,dt_u1_incsp_1,dt_u2_incsp_1,existence_l1_incsp_1,existence_m1_subset_1,t12_projred1,t13_projred1,t1_subset,t2_subset,t6_boole,t7_boole,t8_boole]), [file(projred1,t14_projred1)]). fof(antisymmetry_r2_hidden,axiom,( ! [A,B] : ( r2_hidden(A,B) => ~ r2_hidden(B,A) ) ), file(hidden,r2_hidden), []). fof(cc1_funct_1,axiom,( ! [A] : ( v1_xboole_0(A) => v1_funct_1(A) ) ), file(funct_1,cc1_funct_1), []). fof(d10_incproj,axiom,( ! [A] : ( l1_incsp_1(A) => ( v2_incproj(A) <=> ! [B] : ( m1_subset_1(B,u1_incsp_1(A)) => ! [C] : ( m1_subset_1(C,u1_incsp_1(A)) => ? [D] : ( m1_subset_1(D,u2_incsp_1(A)) & r1_incsp_1(A,B,D) & r1_incsp_1(A,C,D) ) ) ) ) ) ), file(incproj,d10_incproj), []). fof(d19_incproj,axiom,( ! [A] : ( ( v1_incproj(A) & v2_incproj(A) & v3_incproj(A) & v4_incproj(A) & v5_incproj(A) & l1_incsp_1(A) ) => ( v10_incproj(A) <=> ! [B] : ( m1_subset_1(B,u1_incsp_1(A)) => ! [C] : ( m1_subset_1(C,u1_incsp_1(A)) => ! [D] : ( m1_subset_1(D,u1_incsp_1(A)) => ! [E] : ( m1_subset_1(E,u1_incsp_1(A)) => ! [F] : ( m1_subset_1(F,u1_incsp_1(A)) => ! [G] : ( m1_subset_1(G,u1_incsp_1(A)) => ! [H] : ( m1_subset_1(H,u1_incsp_1(A)) => ! [I] : ( m1_subset_1(I,u1_incsp_1(A)) => ! [J] : ( m1_subset_1(J,u1_incsp_1(A)) => ! [K] : ( m1_subset_1(K,u1_incsp_1(A)) => ! [L] : ( m1_subset_1(L,u2_incsp_1(A)) => ! [M] : ( m1_subset_1(M,u2_incsp_1(A)) => ! [N] : ( m1_subset_1(N,u2_incsp_1(A)) => ! [O] : ( m1_subset_1(O,u2_incsp_1(A)) => ! [P] : ( m1_subset_1(P,u2_incsp_1(A)) => ! [Q] : ( m1_subset_1(Q,u2_incsp_1(A)) => ! [R] : ( m1_subset_1(R,u2_incsp_1(A)) => ! [S] : ( m1_subset_1(S,u2_incsp_1(A)) => ! [T] : ( m1_subset_1(T,u2_incsp_1(A)) => ~ ( r4_incproj(A,B,C,L,D) & r4_incproj(A,B,F,M,E) & r4_incproj(A,B,H,N,G) & r4_incproj(A,H,F,O,K) & r4_incproj(A,H,I,P,D) & r4_incproj(A,F,J,Q,D) & r4_incproj(A,K,E,R,G) & r4_incproj(A,C,I,S,G) & r4_incproj(A,C,J,T,E) & r1_incproj(L,M,N) & B != D & B != F & B != H & B != C & B != E & B != G & D != C & F != E & H != G & ! [U] : ( m1_subset_1(U,u2_incsp_1(A)) => ~ r4_incproj(A,I,J,U,K) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ), file(incproj,d19_incproj), []). fof(d5_incproj,axiom,( ! [A,B,C] : ( r1_incproj(A,B,C) <=> ( A != B & B != C & C != A ) ) ), file(incproj,d5_incproj), []). fof(d8_incproj,axiom,( ! [A] : ( l1_incsp_1(A) => ! [B] : ( m1_subset_1(B,u1_incsp_1(A)) => ! [C] : ( m1_subset_1(C,u1_incsp_1(A)) => ! [D] : ( m1_subset_1(D,u2_incsp_1(A)) => ! [E] : ( m1_subset_1(E,u1_incsp_1(A)) => ( r4_incproj(A,B,C,D,E) <=> ( r1_incsp_1(A,B,D) & r1_incsp_1(A,C,D) & r1_incsp_1(A,E,D) ) ) ) ) ) ) ) ), file(incproj,d8_incproj), []). fof(d9_incproj,axiom,( ! [A] : ( l1_incsp_1(A) => ( v1_incproj(A) <=> ! [B] : ( m1_subset_1(B,u1_incsp_1(A)) => ! [C] : ( m1_subset_1(C,u1_incsp_1(A)) => ! [D] : ( m1_subset_1(D,u2_incsp_1(A)) => ! [E] : ( m1_subset_1(E,u2_incsp_1(A)) => ~ ( r1_incsp_1(A,B,D) & r1_incsp_1(A,C,D) & r1_incsp_1(A,B,E) & r1_incsp_1(A,C,E) & B != C & D != E ) ) ) ) ) ) ) ), file(incproj,d9_incproj), []). fof(dt_k1_xboole_0,axiom,( $true ), file(xboole_0,k1_xboole_0), []). fof(dt_l1_incsp_1,axiom,( $true ), file(incsp_1,l1_incsp_1), []). fof(dt_m1_subset_1,axiom,( $true ), file(subset_1,m1_subset_1), []). fof(dt_u1_incsp_1,axiom,( ! [A] : ( l1_incsp_1(A) => ~ v1_xboole_0(u1_incsp_1(A)) ) ), file(incsp_1,u1_incsp_1), []). fof(dt_u2_incsp_1,axiom,( ! [A] : ( l1_incsp_1(A) => ~ v1_xboole_0(u2_incsp_1(A)) ) ), file(incsp_1,u2_incsp_1), []). fof(existence_l1_incsp_1,axiom,( ? [A] : l1_incsp_1(A) ), file(incsp_1,l1_incsp_1), []). fof(existence_m1_subset_1,axiom,( ! [A] : ? [B] : m1_subset_1(B,A) ), file(subset_1,m1_subset_1), []). fof(t12_projred1,axiom,( ! [A] : ( ( v1_incproj(A) & v2_incproj(A) & v3_incproj(A) & v4_incproj(A) & v5_incproj(A) & l1_incsp_1(A) ) => ! [B] : ( m1_subset_1(B,u1_incsp_1(A)) => ! [C] : ( m1_subset_1(C,u1_incsp_1(A)) => ! [D] : ( m1_subset_1(D,u1_incsp_1(A)) => ! [E] : ( m1_subset_1(E,u1_incsp_1(A)) => ! [F] : ( m1_subset_1(F,u2_incsp_1(A)) => ! [G] : ( m1_subset_1(G,u2_incsp_1(A)) => ! [H] : ( m1_subset_1(H,u2_incsp_1(A)) => ! [I] : ( m1_subset_1(I,u2_incsp_1(A)) => ~ ( r1_incsp_1(A,B,F) & r1_incsp_1(A,B,G) & F != G & r1_incsp_1(A,C,F) & B != C & r1_incsp_1(A,D,G) & r1_incsp_1(A,E,G) & D != E & r1_incsp_1(A,C,H) & r1_incsp_1(A,D,H) & r1_incsp_1(A,C,I) & r1_incsp_1(A,E,I) & H = I ) ) ) ) ) ) ) ) ) ) ), file(projred1,t12_projred1), []). fof(t13_projred1,axiom,( ! [A] : ( ( v1_incproj(A) & v2_incproj(A) & v3_incproj(A) & v4_incproj(A) & v5_incproj(A) & l1_incsp_1(A) ) => ! [B] : ( m1_subset_1(B,u1_incsp_1(A)) => ! [C] : ( m1_subset_1(C,u1_incsp_1(A)) => ! [D] : ( m1_subset_1(D,u1_incsp_1(A)) => ! [E] : ( m1_subset_1(E,u2_incsp_1(A)) => ( r4_incproj(A,B,C,E,D) => ( r4_incproj(A,B,D,E,C) & r4_incproj(A,C,B,E,D) & r4_incproj(A,C,D,E,B) & r4_incproj(A,D,B,E,C) & r4_incproj(A,D,C,E,B) ) ) ) ) ) ) ) ), file(projred1,t13_projred1), []). fof(t1_subset,axiom,( ! [A,B] : ( r2_hidden(A,B) => m1_subset_1(A,B) ) ), file(subset,t1_subset), []). fof(t2_subset,axiom,( ! [A,B] : ( m1_subset_1(A,B) => ( v1_xboole_0(B) | r2_hidden(A,B) ) ) ), file(subset,t2_subset), []). fof(t6_boole,axiom,( ! [A] : ( v1_xboole_0(A) => A = k1_xboole_0 ) ), file(boole,t6_boole), []). fof(t7_boole,axiom,( ! [A,B] : ~ ( r2_hidden(A,B) & v1_xboole_0(B) ) ), file(boole,t7_boole), []). fof(t8_boole,axiom,( ! [A,B] : ~ ( v1_xboole_0(A) & A != B & v1_xboole_0(B) ) ), file(boole,t8_boole), []).