fof(t89_orders_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & v3_orders_2(A) & v4_orders_2(A) & l1_orders_2(A) ) => ! [B] : ( m1_orders_1(B,k1_orders_1(u1_struct_0(A))) => m2_orders_2(k3_tarski(k4_orders_2(A,B)),A,B) ) ) ), inference(mizar_proof,[status(thm)],[l104_orders_2,t87_orders_2,d4_orders_2,d5_orders_2,d6_orders_2,t93_orders_1,t94_orders_1,t95_orders_1,d5_wellord1,d11_orders_2,t92_orders_1,d3_wellord1,d3_tarski,d4_tarski,d17_orders_2,d16_orders_2,d3_xboole_0,t17_xboole_1,t9_wellord1,d3_xboole_0,d3_xboole_0,d3_tarski,d3_xboole_0,d1_wellord1,d9_orders_2,d10_orders_2,t88_orders_2,d3_xboole_0,t70_orders_2,d3_xboole_0,d9_orders_2,t25_orders_2,d7_xboole_0,d10_xboole_0,t2_xboole_1,d4_tarski,d17_orders_2,d16_orders_2,t88_orders_2,d16_orders_2,t71_orders_2,d16_orders_2]), [file(orders_2,t89_orders_2),interesting(1.00)]). fof(l183_orders_2,theorem,( ! [A,B,C] : ( v1_relat_1(C) => ( ( r2_wellord1(C,A) & r1_tarski(B,A) ) => r2_wellord1(C,B) ) ) ), inference(mizar_proof,[status(thm)],[d5_wellord1,l182_orders_2,t93_orders_1,t94_orders_1,t95_orders_1,d5_wellord1,d3_wellord1,d5_wellord1,t1_xboole_1,d3_wellord1]), [file(orders_2,l183_orders_2),interesting(0.94)]). fof(l182_orders_2,theorem,( ! [A,B,C] : ( v1_relat_1(C) => ( ( r6_relat_2(C,A) & r1_tarski(B,A) ) => r6_relat_2(C,B) ) ) ), inference(mizar_proof,[status(thm)],[d6_relat_2,d6_relat_2]), [file(orders_2,l182_orders_2),interesting(0.91)]). fof(t28_orders_2,theorem,( ! [A] : ( ( v4_orders_2(A) & l1_orders_2(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ~ ( r2_orders_2(A,B,C) & r2_orders_2(A,C,B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d10_orders_2,t25_orders_2]), [file(orders_2,t28_orders_2),interesting(0.78)]). fof(t30_orders_2,theorem,( ! [A] : ( ( v4_orders_2(A) & l1_orders_2(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ~ ( r1_orders_2(A,B,C) & r2_orders_2(A,C,B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d10_orders_2,t25_orders_2]), [file(orders_2,t30_orders_2),interesting(0.78)]). fof(t162_orders_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & v3_orders_2(A) & v4_orders_2(A) & l1_orders_2(A) ) => ~ ( ! [B] : ( ( v5_orders_2(B,A) & m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) ) => ? [C] : ( m1_subset_1(C,u1_struct_0(A)) & ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( r2_hidden(D,B) => r3_orders_2(A,D,C) ) ) ) ) & ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ? [C] : ( m1_subset_1(C,u1_struct_0(A)) & r2_orders_2(A,B,C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t89_orders_2,t32_orders_2,d1_tarski,d4_xboole_0,t4_orders_1,d1_orders_1,d4_orders_2,d5_orders_2,d6_orders_2,t93_orders_1,t94_orders_1,t95_orders_1,d6_relat_2,t38_orders_2,d9_orders_2,d1_tarski,d10_orders_2,d9_orders_2,d1_tarski,d10_orders_2,d9_orders_2,d1_tarski,d2_xboole_0,d3_wellord1,d1_tarski,t3_xboole_0,d1_tarski,d1_wellord1,d3_tarski,d4_xboole_0,d2_xboole_0,d4_xboole_0,d16_orders_2,l183_orders_2,d5_wellord1,t37_xboole_1,t39_zfmisc_1,d3_wellord1,d7_xboole_0,t36_xboole_1,t37_zfmisc_1,t45_xboole_1,d1_wellord1,d9_orders_2,d10_orders_2,t28_orders_2,d3_xboole_0,d1_tarski,d3_xboole_0,t23_xboole_1,d7_xboole_0,t56_zfmisc_1,t83_xboole_1,d5_wellord1,t92_orders_1,d11_orders_2,d3_tarski,d3_xboole_0,d2_xboole_0,d1_tarski,d3_xboole_0,t50_orders_2,d10_xboole_0,d3_tarski,d2_xboole_0,t52_orders_2,d3_xboole_0,d1_tarski,d2_xboole_0,d3_tarski,d3_xboole_0,d3_xboole_0,d2_xboole_0,d1_tarski,d1_tarski,t28_orders_2,d3_xboole_0,d10_xboole_0,t7_xboole_1,t65_orders_2,d16_orders_2,d16_orders_2,d1_tarski,d17_orders_2,d2_xboole_0,d4_tarski]), [file(orders_2,t162_orders_2),interesting(0.78)]). fof(t25_orders_2,theorem,( ! [A] : ( ( v4_orders_2(A) & l1_orders_2(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( ( r1_orders_2(A,B,C) & r1_orders_2(A,C,B) ) => B = C ) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_orders_2,d6_orders_2,t106_zfmisc_1,d4_relat_2]), [file(orders_2,t25_orders_2),interesting(0.77)]). fof(t26_orders_2,theorem,( ! [A] : ( ( v3_orders_2(A) & l1_orders_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)) => ( ( r1_orders_2(A,B,C) & r1_orders_2(A,C,D) ) => r1_orders_2(A,B,D) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_orders_2,d5_orders_2,t106_zfmisc_1,d8_relat_2,d9_orders_2]), [file(orders_2,t26_orders_2),interesting(0.76)]). fof(t24_orders_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & l1_orders_2(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => r1_orders_2(A,B,B) ) ) ), inference(mizar_proof,[status(thm)],[d4_orders_2,d1_relat_2,d9_orders_2]), [file(orders_2,t24_orders_2),interesting(0.72)]). fof(t40_orders_2,theorem,( ! [A] : ( l1_orders_2(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ( r2_wellord1(u1_orders_2(A),B) => ( v5_orders_2(B,A) & m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d5_wellord1,t92_orders_1,d11_orders_2]), [file(orders_2,t40_orders_2),interesting(0.69)]). fof(t84_orders_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & v3_orders_2(A) & v4_orders_2(A) & l1_orders_2(A) ) => ! [B] : ( m1_orders_1(B,k1_orders_1(u1_struct_0(A))) => ! [C] : ( m2_orders_2(C,A,B) => ! [D] : ( m2_orders_2(D,A,B) => ( r2_xboole_0(C,D) <=> m1_orders_2(C,A,D) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d8_xboole_0,d16_orders_2,d15_orders_2,t61_orders_2,d10_xboole_0,t83_orders_2,d16_orders_2,d15_orders_2,t61_orders_2,t68_orders_2,d8_xboole_0]), [file(orders_2,t84_orders_2),interesting(0.68)]). fof(t35_orders_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & l1_orders_2(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ( v5_orders_2(k1_struct_0(A,B),A) & m1_subset_1(k1_struct_0(A,B),k1_zfmisc_1(u1_struct_0(A))) ) ) ) ), inference(mizar_proof,[status(thm)],[d4_orders_2,d7_relat_2,d11_orders_2,d1_tarski,d1_relat_2]), [file(orders_2,t35_orders_2),interesting(0.68)]). fof(t43_orders_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & v3_orders_2(A) & v4_orders_2(A) & l1_orders_2(A) ) => k1_orders_2(A,k1_pre_topc(A)) = u1_struct_0(A) ) ), inference(mizar_proof,[status(thm)],[d10_xboole_0,d3_tarski]), [file(orders_2,t43_orders_2),interesting(0.68)]). fof(t32_orders_2,theorem,( ! [A] : ( ( v3_orders_2(A) & v4_orders_2(A) & l1_orders_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)) => ( ( ( r2_orders_2(A,B,C) & r1_orders_2(A,C,D) ) | ( r1_orders_2(A,B,C) & r2_orders_2(A,C,D) ) ) => r2_orders_2(A,B,D) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d10_orders_2,t26_orders_2,t25_orders_2,d10_orders_2,d10_orders_2,t26_orders_2,t25_orders_2,d10_orders_2]), [file(orders_2,t32_orders_2),interesting(0.68)]). fof(t29_orders_2,theorem,( ! [A] : ( ( v3_orders_2(A) & v4_orders_2(A) & l1_orders_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)) => ( ( r2_orders_2(A,B,C) & r2_orders_2(A,C,D) ) => r2_orders_2(A,B,D) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d10_orders_2,t26_orders_2,d10_orders_2,t28_orders_2]), [file(orders_2,t29_orders_2),interesting(0.66)]). fof(t163_orders_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & v3_orders_2(A) & v4_orders_2(A) & l1_orders_2(A) ) => ~ ( ! [B] : ( ( v5_orders_2(B,A) & m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) ) => ? [C] : ( m1_subset_1(C,u1_struct_0(A)) & ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( r2_hidden(D,B) => r3_orders_2(A,C,D) ) ) ) ) & ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ? [C] : ( m1_subset_1(C,u1_struct_0(A)) & r2_orders_2(A,C,B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d7_relat_1,d9_orders_2,t29_relat_2,d4_partfun1,d4_partfun1,t27_relat_2,t40_relat_2,t42_relat_2,d7_relat_2,t38_orders_2,d9_orders_2,d9_orders_2,d9_orders_2,d11_orders_2,d9_orders_2,t162_orders_2,d10_orders_2,d9_orders_2,d10_orders_2]), [file(orders_2,t163_orders_2),interesting(0.65)]). fof(t83_orders_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & v3_orders_2(A) & v4_orders_2(A) & l1_orders_2(A) ) => ! [B] : ( m1_orders_1(B,k1_orders_1(u1_struct_0(A))) => ! [C] : ( m2_orders_2(C,A,B) => ! [D] : ( m2_orders_2(D,A,B) => ( C != D => ( m1_orders_2(C,A,D) <=> ~ m1_orders_2(D,A,C) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,d3_xboole_0,t1_xboole_1,d16_orders_2,t57_orders_2,d3_xboole_0,d3_xboole_0,d3_tarski,t57_orders_2,t29_orders_2,t57_orders_2,t57_orders_2,t57_orders_2,t57_orders_2,d10_xboole_0,d3_tarski,t57_orders_2,t29_orders_2,t57_orders_2,t57_orders_2,t57_orders_2,t57_orders_2,d16_orders_2,d3_tarski,d3_xboole_0,t57_orders_2,d3_xboole_0,d3_xboole_0,d3_tarski,t57_orders_2,t29_orders_2,t57_orders_2,t57_orders_2,t57_orders_2,t57_orders_2,d10_xboole_0,d3_tarski,t57_orders_2,t29_orders_2,t57_orders_2,t57_orders_2,t57_orders_2,t57_orders_2,d16_orders_2,t69_orders_2,d16_orders_2,t69_orders_2,d16_orders_2,d15_orders_2,d16_orders_2,d15_orders_2,d16_orders_2,d16_orders_2,d3_xboole_0,t62_orders_2,t73_orders_2]), [file(orders_2,t83_orders_2),interesting(0.64)]). fof(t67_orders_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & v3_orders_2(A) & v4_orders_2(A) & l1_orders_2(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ! [C] : ( m1_orders_2(C,A,B) => r1_tarski(C,B) ) ) ) ), inference(mizar_proof,[status(thm)],[d15_orders_2,d15_orders_2,t17_xboole_1]), [file(orders_2,t67_orders_2),interesting(0.63)]). fof(t62_orders_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & v3_orders_2(A) & v4_orders_2(A) & l1_orders_2(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ~ r2_hidden(B,k3_orders_2(A,C,B)) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_xboole_0,d1_tarski]), [file(orders_2,t62_orders_2),interesting(0.62)]). fof(t78_orders_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & v3_orders_2(A) & v4_orders_2(A) & l1_orders_2(A) ) => ! [B] : ( m1_orders_1(B,k1_orders_1(u1_struct_0(A))) => m2_orders_2(k1_tarski(k1_funct_1(B,u1_struct_0(A))),A,B) ) ) ), inference(mizar_proof,[status(thm)],[t4_orders_1,t5_orders_1,d1_orders_1,t35_orders_2,d4_orders_2,d5_orders_2,d6_orders_2,t93_orders_1,t94_orders_1,t95_orders_1,d11_orders_2,t92_orders_1,d3_wellord1,t39_zfmisc_1,d1_tarski,d3_tarski,d3_xboole_0,d1_tarski,d3_xboole_0,d1_wellord1,d7_xboole_0,d10_xboole_0,t2_xboole_1,d5_wellord1,d1_tarski,d3_tarski,d3_xboole_0,d3_xboole_0,d10_xboole_0,t2_xboole_1,t43_orders_2,d16_orders_2]), [file(orders_2,t78_orders_2),interesting(0.62)]). fof(t50_orders_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & v3_orders_2(A) & v4_orders_2(A) & l1_orders_2(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ~ r2_hidden(B,k2_orders_2(A,k1_struct_0(A,B))) ) ) ), inference(mizar_proof,[status(thm)],[d1_tarski,t49_orders_2]), [file(orders_2,t50_orders_2),interesting(0.61)]). fof(t87_orders_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & v3_orders_2(A) & v4_orders_2(A) & l1_orders_2(A) ) => ! [B] : ( m1_orders_1(B,k1_orders_1(u1_struct_0(A))) => k3_tarski(k4_orders_2(A,B)) != k1_xboole_0 ) ) ), inference(mizar_proof,[status(thm)],[t78_orders_2,d17_orders_2,t91_orders_1]), [file(orders_2,t87_orders_2),interesting(0.60)]). fof(t79_orders_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & v3_orders_2(A) & v4_orders_2(A) & l1_orders_2(A) ) => ! [B] : ( m1_orders_1(B,k1_orders_1(u1_struct_0(A))) => ! [C] : ( m2_orders_2(C,A,B) => r2_hidden(k1_funct_1(B,u1_struct_0(A)),C) ) ) ) ), inference(mizar_proof,[status(thm)],[d16_orders_2,t9_wellord1,d3_xboole_0,l7_orders_2,d9_orders_2,d3_xboole_0,d1_tarski,t30_orders_2,d16_orders_2,t43_orders_2]), [file(orders_2,t79_orders_2),interesting(0.60)]). fof(t107_orders_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & v3_orders_2(A) & v4_orders_2(A) & l1_orders_2(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => k3_relat_1(k2_wellord1(u1_orders_2(A),B)) = B ) ) ), inference(mizar_proof,[status(thm)],[t20_wellord1,d10_xboole_0,d3_tarski,d4_orders_2,d1_relat_2,t106_zfmisc_1,t16_wellord1,d4_relat_1,d5_relat_1,d2_xboole_0,d6_relat_1]), [file(orders_2,t107_orders_2),interesting(0.58)]). fof(t61_orders_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & v3_orders_2(A) & v4_orders_2(A) & l1_orders_2(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => r1_tarski(k3_orders_2(A,C,B),C) ) ) ) ), inference(mizar_proof,[status(thm)],[t17_xboole_1]), [file(orders_2,t61_orders_2),interesting(0.57)]). fof(l104_orders_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & v3_orders_2(A) & v4_orders_2(A) & l1_orders_2(A) ) => ! [B] : ( m1_orders_1(B,k1_orders_1(u1_struct_0(A))) => ( v5_orders_2(k3_tarski(k4_orders_2(A,B)),A) & m1_subset_1(k3_tarski(k4_orders_2(A,B)),k1_zfmisc_1(u1_struct_0(A))) ) ) ) ), inference(mizar_proof,[status(thm)],[l103_orders_2,d7_relat_2,d4_tarski,d4_tarski,d17_orders_2,d11_orders_2,d11_orders_2,d7_relat_2,t84_orders_2,d8_xboole_0,d7_relat_2,t84_orders_2,d8_xboole_0,d7_relat_2,t83_orders_2,d11_orders_2]), [file(orders_2,l104_orders_2),interesting(0.57)]). fof(t68_orders_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & v3_orders_2(A) & v4_orders_2(A) & l1_orders_2(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ( ~ ( B != k1_xboole_0 & m1_orders_2(B,A,B) ) & ~ ( ~ m1_orders_2(B,A,B) & B = k1_xboole_0 ) ) ) ) ), inference(mizar_proof,[status(thm)],[d15_orders_2,d3_xboole_0,t50_orders_2,d15_orders_2]), [file(orders_2,t68_orders_2),interesting(0.56)]). fof(t45_orders_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & v3_orders_2(A) & v4_orders_2(A) & l1_orders_2(A) ) => k2_orders_2(A,k1_pre_topc(A)) = u1_struct_0(A) ) ), inference(mizar_proof,[status(thm)],[d10_xboole_0,d3_tarski]), [file(orders_2,t45_orders_2),interesting(0.54)]). fof(t37_orders_2,theorem,( ! [A] : ( l1_orders_2(A) => ! [B] : ( ( v5_orders_2(B,A) & m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) ) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ( r1_tarski(C,B) => ( v5_orders_2(C,A) & m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d11_orders_2,t96_orders_1,d11_orders_2]), [file(orders_2,t37_orders_2),interesting(0.53)]). fof(t44_orders_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & v3_orders_2(A) & v4_orders_2(A) & l1_orders_2(A) ) => k1_orders_2(A,k2_pre_topc(A)) = k1_xboole_0 ) ), inference(mizar_proof,[status(thm)],[d3_tarski,t12_pre_topc,d10_xboole_0,t2_xboole_1]), [file(orders_2,t44_orders_2),interesting(0.52)]). fof(t46_orders_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & v3_orders_2(A) & v4_orders_2(A) & l1_orders_2(A) ) => k2_orders_2(A,k2_pre_topc(A)) = k1_xboole_0 ) ), inference(mizar_proof,[status(thm)],[d3_tarski,t12_pre_topc,d10_xboole_0,t2_xboole_1]), [file(orders_2,t46_orders_2),interesting(0.52)]). fof(t82_orders_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & v3_orders_2(A) & v4_orders_2(A) & l1_orders_2(A) ) => ! [B] : ( m1_orders_1(B,k1_orders_1(u1_struct_0(A))) => ! [C] : ( m2_orders_2(C,A,B) => ! [D] : ( m2_orders_2(D,A,B) => ~ r1_xboole_0(C,D) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t79_orders_2,t3_xboole_0]), [file(orders_2,t82_orders_2),interesting(0.52)]). fof(t71_orders_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & v3_orders_2(A) & v4_orders_2(A) & l1_orders_2(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) => ( ( r2_hidden(B,C) & m1_orders_2(C,A,D) ) => k3_orders_2(A,C,B) = k3_orders_2(A,D,B) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t67_orders_2,d3_tarski,d3_xboole_0,d3_xboole_0,d10_xboole_0,d3_tarski,d3_xboole_0,d1_tarski,d3_xboole_0,t70_orders_2,d3_xboole_0]), [file(orders_2,t71_orders_2),interesting(0.47)]). fof(t136_orders_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & v3_orders_2(A) & v4_orders_2(A) & l1_orders_2(A) ) => ! [B] : ( ( v5_orders_2(B,A) & m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) ) => r3_orders_1(u1_orders_2(A),B) ) ) ), inference(mizar_proof,[status(thm)],[d4_orders_2,d5_orders_2,d6_orders_2,t93_orders_1,t94_orders_1,t95_orders_1,d8_orders_1,d11_orders_2,t92_orders_1]), [file(orders_2,t136_orders_2),interesting(0.46)]). fof(l103_orders_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & v3_orders_2(A) & v4_orders_2(A) & l1_orders_2(A) ) => ! [B] : ( m1_orders_1(B,k1_orders_1(u1_struct_0(A))) => m1_subset_1(k3_tarski(k4_orders_2(A,B)),k1_zfmisc_1(u1_struct_0(A))) ) ) ), inference(mizar_proof,[status(thm)],[d17_orders_2,t94_zfmisc_1]), [file(orders_2,l103_orders_2),interesting(0.46)]). fof(t48_orders_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & v3_orders_2(A) & v4_orders_2(A) & l1_orders_2(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ~ r2_hidden(B,k1_orders_2(A,k1_struct_0(A,B))) ) ) ), inference(mizar_proof,[status(thm)],[d1_tarski,t47_orders_2]), [file(orders_2,t48_orders_2),interesting(0.46)]). fof(t52_orders_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & v3_orders_2(A) & v4_orders_2(A) & l1_orders_2(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( r2_orders_2(A,B,C) <=> r2_hidden(B,k2_orders_2(A,k1_struct_0(A,C))) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_tarski,d1_tarski]), [file(orders_2,t52_orders_2),interesting(0.45)]). fof(t109_orders_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & v3_orders_2(A) & v4_orders_2(A) & l1_orders_2(A) ) => ! [B] : ( ( v5_orders_2(B,A) & m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) ) => v3_orders_1(k2_wellord1(u1_orders_2(A),B)) ) ) ), inference(mizar_proof,[status(thm)],[d4_orders_1,t114_orders_1,d4_orders_1,d5_orders_1,t107_orders_2,d6_relat_2,d11_orders_2,d7_relat_2,t106_zfmisc_1,t16_wellord1,d14_relat_2]), [file(orders_2,t109_orders_2),interesting(0.43)]). fof(t158_orders_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & v3_orders_2(A) & v4_orders_2(A) & l1_orders_2(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ( r7_orders_1(u1_orders_2(A),B) <=> ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ~ r2_orders_2(A,C,B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t100_orders_1,d12_orders_1,d9_orders_2,d10_orders_2,d12_orders_1,t100_orders_1,d9_orders_2,d10_orders_2]), [file(orders_2,t158_orders_2),interesting(0.43)]). fof(t159_orders_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & v3_orders_2(A) & v4_orders_2(A) & l1_orders_2(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ( r6_orders_1(u1_orders_2(A),B) <=> ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ~ r2_orders_2(A,B,C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t100_orders_1,d11_orders_1,d9_orders_2,d10_orders_2,d11_orders_1,t100_orders_1,d9_orders_2,d10_orders_2]), [file(orders_2,t159_orders_2),interesting(0.43)]). fof(t88_orders_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & v3_orders_2(A) & v4_orders_2(A) & l1_orders_2(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ! [C] : ( m1_orders_1(C,k1_orders_1(u1_struct_0(A))) => ! [D] : ( m2_orders_2(D,A,C) => ( B = k3_tarski(k4_orders_2(A,C)) => ( D = k3_tarski(k4_orders_2(A,C)) | m1_orders_2(D,A,B) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d17_orders_2,t92_zfmisc_1,d10_xboole_0,t37_xboole_1,d4_xboole_0,d4_tarski,d17_orders_2,d4_xboole_0,d4_xboole_0,d8_xboole_0,t84_orders_2,t83_orders_2,d15_orders_2,t92_zfmisc_1,d3_tarski,d3_xboole_0,d1_tarski,d3_xboole_0,d4_tarski,d17_orders_2,d3_xboole_0,t70_orders_2,d3_xboole_0,t84_orders_2,d8_xboole_0,d3_xboole_0,t83_orders_2,d10_xboole_0,d3_tarski,d3_xboole_0,d3_xboole_0,d15_orders_2]), [file(orders_2,t88_orders_2),interesting(0.43)]). fof(t80_orders_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & v3_orders_2(A) & v4_orders_2(A) & l1_orders_2(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_orders_1(D,k1_orders_1(u1_struct_0(A))) => ! [E] : ( m2_orders_2(E,A,D) => ( ( r2_hidden(B,E) & C = k1_funct_1(D,u1_struct_0(A)) ) => r3_orders_2(A,C,B) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d16_orders_2,t9_wellord1,d3_xboole_0,l7_orders_2,d9_orders_2,d3_xboole_0,d1_tarski,t30_orders_2,d16_orders_2,t43_orders_2,d9_orders_2]), [file(orders_2,t80_orders_2),interesting(0.37)]). fof(t160_orders_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & v3_orders_2(A) & v4_orders_2(A) & l1_orders_2(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ( r8_orders_1(u1_orders_2(A),B) <=> ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( B != C => r2_orders_2(A,C,B) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t100_orders_1,d13_orders_1,d9_orders_2,d10_orders_2,d13_orders_1,t100_orders_1,d10_orders_2,d9_orders_2]), [file(orders_2,t160_orders_2),interesting(0.36)]). fof(t161_orders_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & v3_orders_2(A) & v4_orders_2(A) & l1_orders_2(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ( r9_orders_1(u1_orders_2(A),B) <=> ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( B != C => r2_orders_2(A,B,C) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t100_orders_1,d14_orders_1,d9_orders_2,d10_orders_2,d14_orders_1,t100_orders_1,d10_orders_2,d9_orders_2]), [file(orders_2,t161_orders_2),interesting(0.36)]). fof(t108_orders_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & v3_orders_2(A) & v4_orders_2(A) & l1_orders_2(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ( v3_orders_1(k2_wellord1(u1_orders_2(A),B)) => ( v5_orders_2(B,A) & m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t107_orders_2,d5_orders_1,d14_relat_2,d7_relat_2,d11_orders_2,d9_orders_2,d6_relat_2,t16_wellord1]), [file(orders_2,t108_orders_2),interesting(0.35)]). fof(t51_orders_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & v3_orders_2(A) & v4_orders_2(A) & l1_orders_2(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( r2_orders_2(A,B,C) <=> r2_hidden(C,k1_orders_2(A,k1_struct_0(A,B))) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_tarski,d1_tarski]), [file(orders_2,t51_orders_2),interesting(0.34)]). fof(t135_orders_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & v3_orders_2(A) & v4_orders_2(A) & l1_orders_2(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ( r3_orders_1(u1_orders_2(A),B) => ( v5_orders_2(B,A) & m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d8_orders_1,t92_orders_1,d11_orders_2]), [file(orders_2,t135_orders_2),interesting(0.33)]). fof(t56_orders_2,theorem,( ! [A,B] : ( ( ~ v3_struct_0(B) & v2_orders_2(B) & v3_orders_2(B) & v4_orders_2(B) & l1_orders_2(B) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(B)) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(B))) => ( r2_hidden(A,k3_orders_2(B,D,C)) <=> ( r2_hidden(A,k2_orders_2(B,k1_struct_0(B,C))) & r2_hidden(A,D) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_xboole_0]), [file(orders_2,t56_orders_2),interesting(0.32)]). fof(t73_orders_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & v3_orders_2(A) & v4_orders_2(A) & l1_orders_2(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ~ ( r1_tarski(B,C) & r2_wellord1(u1_orders_2(A),C) & ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ( ( r2_hidden(E,B) & r2_hidden(D,C) & r2_orders_2(A,D,E) ) => r2_hidden(D,B) ) ) ) & B != C & ~ m1_orders_2(B,A,C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d10_xboole_0,t36_xboole_1,t37_xboole_1,t9_wellord1,d4_xboole_0,d3_tarski,t40_orders_2,d1_tarski,t39_orders_2,d4_xboole_0,d10_orders_2,d4_xboole_0,d3_xboole_0,d10_xboole_0,d3_tarski,d3_xboole_0,d9_orders_2,d1_tarski,t30_orders_2,d3_xboole_0,d4_xboole_0,t3_xboole_1,d15_orders_2]), [file(orders_2,t73_orders_2),interesting(0.21)]). fof(t81_orders_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & v3_orders_2(A) & v4_orders_2(A) & l1_orders_2(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_orders_1(C,k1_orders_1(u1_struct_0(A))) => ! [D] : ( m2_orders_2(D,A,C) => ( B = k1_funct_1(C,u1_struct_0(A)) => k3_orders_2(A,D,B) = k1_xboole_0 ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t79_orders_2,d3_xboole_0,l7_orders_2,d3_xboole_0,d1_tarski,t80_orders_2,t39_orders_2]), [file(orders_2,t81_orders_2),interesting(0.20)]). fof(t100_orders_2,theorem,( $true ), file(orders_2,t100_orders_2), [interesting(0.00)]). fof(t101_orders_2,theorem,( $true ), file(orders_2,t101_orders_2), [interesting(0.00)]). fof(t102_orders_2,theorem,( $true ), file(orders_2,t102_orders_2), [interesting(0.00)]). fof(t103_orders_2,theorem,( $true ), file(orders_2,t103_orders_2), [interesting(0.00)]). fof(t104_orders_2,theorem,( $true ), file(orders_2,t104_orders_2), [interesting(0.00)]). fof(t105_orders_2,theorem,( $true ), file(orders_2,t105_orders_2), [interesting(0.00)]). fof(t106_orders_2,theorem,( $true ), file(orders_2,t106_orders_2), [interesting(0.00)]). fof(t20_wellord1,theorem,( ! [A,B] : ( v1_relat_1(B) => ( r1_tarski(k3_relat_1(k2_wellord1(B,A)),k3_relat_1(B)) & r1_tarski(k3_relat_1(k2_wellord1(B,A)),A) ) ) ), file(wellord1,t20_wellord1), [interesting(0.00)]). fof(d10_xboole_0,definition,( ! [A,B] : ( A = B <=> ( r1_tarski(A,B) & r1_tarski(B,A) ) ) ), file(xboole_0,d10_xboole_0), [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(d4_orders_2,definition,( ! [A] : ( l1_orders_2(A) => ( v2_orders_2(A) <=> r1_relat_2(u1_orders_2(A),u1_struct_0(A)) ) ) ), file(orders_2,d4_orders_2), [interesting(0.00)]). fof(d1_relat_2,definition,( ! [A] : ( v1_relat_1(A) => ! [B] : ( r1_relat_2(A,B) <=> ! [C] : ( r2_hidden(C,B) => r2_hidden(k4_tarski(C,C),A) ) ) ) ), file(relat_2,d1_relat_2), [interesting(0.00)]). fof(t106_zfmisc_1,theorem,( ! [A,B,C,D] : ( r2_hidden(k4_tarski(A,B),k2_zfmisc_1(C,D)) <=> ( r2_hidden(A,C) & r2_hidden(B,D) ) ) ), file(zfmisc_1,t106_zfmisc_1), [interesting(0.00)]). fof(t16_wellord1,theorem,( ! [A,B,C] : ( v1_relat_1(C) => ( r2_hidden(A,k2_wellord1(C,B)) <=> ( r2_hidden(A,C) & r2_hidden(A,k2_zfmisc_1(B,B)) ) ) ) ), file(wellord1,t16_wellord1), [interesting(0.00)]). fof(d4_relat_1,definition,( ! [A] : ( v1_relat_1(A) => ! [B] : ( B = k1_relat_1(A) <=> ! [C] : ( r2_hidden(C,B) <=> ? [D] : r2_hidden(k4_tarski(C,D),A) ) ) ) ), file(relat_1,d4_relat_1), [interesting(0.00)]). fof(d5_relat_1,definition,( ! [A] : ( v1_relat_1(A) => ! [B] : ( B = k2_relat_1(A) <=> ! [C] : ( r2_hidden(C,B) <=> ? [D] : r2_hidden(k4_tarski(D,C),A) ) ) ) ), file(relat_1,d5_relat_1), [interesting(0.00)]). fof(d2_xboole_0,definition,( ! [A,B,C] : ( C = k2_xboole_0(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ( r2_hidden(D,A) | r2_hidden(D,B) ) ) ) ), file(xboole_0,d2_xboole_0), [interesting(0.00)]). fof(d6_relat_1,definition,( ! [A] : ( v1_relat_1(A) => k3_relat_1(A) = k2_xboole_0(k1_relat_1(A),k2_relat_1(A)) ) ), file(relat_1,d6_relat_1), [interesting(0.00)]). fof(d5_orders_1,definition,( ! [A] : ( v1_relat_1(A) => ( v3_orders_1(A) <=> ( v1_relat_2(A) & v8_relat_2(A) & v4_relat_2(A) & v6_relat_2(A) ) ) ) ), file(orders_1,d5_orders_1), [interesting(0.00)]). fof(d14_relat_2,definition,( ! [A] : ( v1_relat_1(A) => ( v6_relat_2(A) <=> r6_relat_2(A,k3_relat_1(A)) ) ) ), file(relat_2,d14_relat_2), [interesting(0.00)]). fof(d7_relat_2,definition,( ! [A] : ( v1_relat_1(A) => ! [B] : ( r7_relat_2(A,B) <=> ! [C,D] : ~ ( r2_hidden(C,B) & r2_hidden(D,B) & ~ r2_hidden(k4_tarski(C,D),A) & ~ r2_hidden(k4_tarski(D,C),A) ) ) ) ), file(relat_2,d7_relat_2), [interesting(0.00)]). fof(d11_orders_2,definition,( ! [A] : ( l1_orders_2(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ( v5_orders_2(B,A) <=> r7_relat_2(u1_orders_2(A),B) ) ) ) ), file(orders_2,d11_orders_2), [interesting(0.00)]). fof(d9_orders_2,definition,( ! [A] : ( l1_orders_2(A) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( r1_orders_2(A,B,C) <=> r2_hidden(k4_tarski(B,C),u1_orders_2(A)) ) ) ) ) ), file(orders_2,d9_orders_2), [interesting(0.00)]). fof(d6_relat_2,definition,( ! [A] : ( v1_relat_1(A) => ! [B] : ( r6_relat_2(A,B) <=> ! [C,D] : ~ ( r2_hidden(C,B) & r2_hidden(D,B) & C != D & ~ r2_hidden(k4_tarski(C,D),A) & ~ r2_hidden(k4_tarski(D,C),A) ) ) ) ), file(relat_2,d6_relat_2), [interesting(0.00)]). fof(d4_orders_1,definition,( ! [A] : ( v1_relat_1(A) => ( v2_orders_1(A) <=> ( v1_relat_2(A) & v8_relat_2(A) & v4_relat_2(A) ) ) ) ), file(orders_1,d4_orders_1), [interesting(0.00)]). fof(t114_orders_1,theorem,( ! [A] : ( v1_relat_1(A) => ! [B] : ( v2_orders_1(A) => v2_orders_1(k2_wellord1(A,B)) ) ) ), file(orders_1,t114_orders_1), [interesting(0.00)]). fof(t10_orders_2,theorem,( $true ), file(orders_2,t10_orders_2), [interesting(0.00)]). fof(t110_orders_2,theorem,( $true ), file(orders_2,t110_orders_2), [interesting(0.00)]). fof(t111_orders_2,theorem,( $true ), file(orders_2,t111_orders_2), [interesting(0.00)]). fof(t112_orders_2,theorem,( $true ), file(orders_2,t112_orders_2), [interesting(0.00)]). fof(t113_orders_2,theorem,( $true ), file(orders_2,t113_orders_2), [interesting(0.00)]). fof(t114_orders_2,theorem,( $true ), file(orders_2,t114_orders_2), [interesting(0.00)]). fof(t115_orders_2,theorem,( $true ), file(orders_2,t115_orders_2), [interesting(0.00)]). fof(t116_orders_2,theorem,( $true ), file(orders_2,t116_orders_2), [interesting(0.00)]). fof(t117_orders_2,theorem,( $true ), file(orders_2,t117_orders_2), [interesting(0.00)]). fof(t118_orders_2,theorem,( $true ), file(orders_2,t118_orders_2), [interesting(0.00)]). fof(t119_orders_2,theorem,( $true ), file(orders_2,t119_orders_2), [interesting(0.00)]). fof(t11_orders_2,theorem,( $true ), file(orders_2,t11_orders_2), [interesting(0.00)]). fof(t120_orders_2,theorem,( $true ), file(orders_2,t120_orders_2), [interesting(0.00)]). fof(t121_orders_2,theorem,( $true ), file(orders_2,t121_orders_2), [interesting(0.00)]). fof(t122_orders_2,theorem,( $true ), file(orders_2,t122_orders_2), [interesting(0.00)]). fof(t123_orders_2,theorem,( $true ), file(orders_2,t123_orders_2), [interesting(0.00)]). fof(t124_orders_2,theorem,( $true ), file(orders_2,t124_orders_2), [interesting(0.00)]). fof(t125_orders_2,theorem,( $true ), file(orders_2,t125_orders_2), [interesting(0.00)]). fof(t126_orders_2,theorem,( $true ), file(orders_2,t126_orders_2), [interesting(0.00)]). fof(t127_orders_2,theorem,( $true ), file(orders_2,t127_orders_2), [interesting(0.00)]). fof(t128_orders_2,theorem,( $true ), file(orders_2,t128_orders_2), [interesting(0.00)]). fof(t129_orders_2,theorem,( $true ), file(orders_2,t129_orders_2), [interesting(0.00)]). fof(t12_orders_2,theorem,( $true ), file(orders_2,t12_orders_2), [interesting(0.00)]). fof(t130_orders_2,theorem,( $true ), file(orders_2,t130_orders_2), [interesting(0.00)]). fof(t131_orders_2,theorem,( $true ), file(orders_2,t131_orders_2), [interesting(0.00)]). fof(t132_orders_2,theorem,( $true ), file(orders_2,t132_orders_2), [interesting(0.00)]). fof(t133_orders_2,theorem,( $true ), file(orders_2,t133_orders_2), [interesting(0.00)]). fof(t134_orders_2,theorem,( $true ), file(orders_2,t134_orders_2), [interesting(0.00)]). fof(d8_orders_1,definition,( ! [A] : ( v1_relat_1(A) => ! [B] : ( r3_orders_1(A,B) <=> ( r1_relat_2(A,B) & r8_relat_2(A,B) & r4_relat_2(A,B) & r6_relat_2(A,B) ) ) ) ), file(orders_1,d8_orders_1), [interesting(0.00)]). fof(t92_orders_1,theorem,( ! [A,B] : ( v1_relat_1(B) => ( r7_relat_2(B,A) <=> ( r1_relat_2(B,A) & r6_relat_2(B,A) ) ) ) ), file(orders_1,t92_orders_1), [interesting(0.00)]). fof(d5_orders_2,definition,( ! [A] : ( l1_orders_2(A) => ( v3_orders_2(A) <=> r8_relat_2(u1_orders_2(A),u1_struct_0(A)) ) ) ), file(orders_2,d5_orders_2), [interesting(0.00)]). fof(d6_orders_2,definition,( ! [A] : ( l1_orders_2(A) => ( v4_orders_2(A) <=> r4_relat_2(u1_orders_2(A),u1_struct_0(A)) ) ) ), file(orders_2,d6_orders_2), [interesting(0.00)]). fof(t93_orders_1,theorem,( ! [A,B,C] : ( v1_relat_1(C) => ( ( r1_relat_2(C,A) & r1_tarski(B,A) ) => r1_relat_2(C,B) ) ) ), file(orders_1,t93_orders_1), [interesting(0.00)]). fof(t94_orders_1,theorem,( ! [A,B,C] : ( v1_relat_1(C) => ( ( r4_relat_2(C,A) & r1_tarski(B,A) ) => r4_relat_2(C,B) ) ) ), file(orders_1,t94_orders_1), [interesting(0.00)]). fof(t95_orders_1,theorem,( ! [A,B,C] : ( v1_relat_1(C) => ( ( r8_relat_2(C,A) & r1_tarski(B,A) ) => r8_relat_2(C,B) ) ) ), file(orders_1,t95_orders_1), [interesting(0.00)]). fof(t137_orders_2,theorem,( $true ), file(orders_2,t137_orders_2), [interesting(0.00)]). fof(t138_orders_2,theorem,( $true ), file(orders_2,t138_orders_2), [interesting(0.00)]). fof(t139_orders_2,theorem,( $true ), file(orders_2,t139_orders_2), [interesting(0.00)]). fof(t13_orders_2,theorem,( $true ), file(orders_2,t13_orders_2), [interesting(0.00)]). fof(t140_orders_2,theorem,( $true ), file(orders_2,t140_orders_2), [interesting(0.00)]). fof(t141_orders_2,theorem,( $true ), file(orders_2,t141_orders_2), [interesting(0.00)]). fof(t142_orders_2,theorem,( $true ), file(orders_2,t142_orders_2), [interesting(0.00)]). fof(t143_orders_2,theorem,( $true ), file(orders_2,t143_orders_2), [interesting(0.00)]). fof(t144_orders_2,theorem,( $true ), file(orders_2,t144_orders_2), [interesting(0.00)]). fof(t145_orders_2,theorem,( $true ), file(orders_2,t145_orders_2), [interesting(0.00)]). fof(t146_orders_2,theorem,( $true ), file(orders_2,t146_orders_2), [interesting(0.00)]). fof(t147_orders_2,theorem,( $true ), file(orders_2,t147_orders_2), [interesting(0.00)]). fof(t148_orders_2,theorem,( $true ), file(orders_2,t148_orders_2), [interesting(0.00)]). fof(t149_orders_2,theorem,( $true ), file(orders_2,t149_orders_2), [interesting(0.00)]). fof(t14_orders_2,theorem,( $true ), file(orders_2,t14_orders_2), [interesting(0.00)]). fof(t150_orders_2,theorem,( $true ), file(orders_2,t150_orders_2), [interesting(0.00)]). fof(t151_orders_2,theorem,( $true ), file(orders_2,t151_orders_2), [interesting(0.00)]). fof(t152_orders_2,theorem,( $true ), file(orders_2,t152_orders_2), [interesting(0.00)]). fof(t153_orders_2,theorem,( $true ), file(orders_2,t153_orders_2), [interesting(0.00)]). fof(t154_orders_2,theorem,( $true ), file(orders_2,t154_orders_2), [interesting(0.00)]). fof(t155_orders_2,theorem,( $true ), file(orders_2,t155_orders_2), [interesting(0.00)]). fof(t156_orders_2,theorem,( $true ), file(orders_2,t156_orders_2), [interesting(0.00)]). fof(t157_orders_2,theorem,( $true ), file(orders_2,t157_orders_2), [interesting(0.00)]). fof(t100_orders_1,theorem,( ! [A,B] : ( ( v1_relat_2(B) & v4_relat_2(B) & v8_relat_2(B) & v1_partfun1(B,A,A) & m2_relset_1(B,A,A) ) => k3_relat_1(B) = A ) ), file(orders_1,t100_orders_1), [interesting(0.00)]). fof(d12_orders_1,definition,( ! [A] : ( v1_relat_1(A) => ! [B] : ( r7_orders_1(A,B) <=> ( r2_hidden(B,k3_relat_1(A)) & ! [C] : ~ ( r2_hidden(C,k3_relat_1(A)) & C != B & r2_hidden(k4_tarski(C,B),A) ) ) ) ) ), file(orders_1,d12_orders_1), [interesting(0.00)]). fof(d10_orders_2,definition,( ! [A] : ( l1_orders_2(A) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( r2_orders_2(A,B,C) <=> ( r1_orders_2(A,B,C) & B != C ) ) ) ) ) ), file(orders_2,d10_orders_2), [interesting(0.00)]). fof(d11_orders_1,definition,( ! [A] : ( v1_relat_1(A) => ! [B] : ( r6_orders_1(A,B) <=> ( r2_hidden(B,k3_relat_1(A)) & ! [C] : ~ ( r2_hidden(C,k3_relat_1(A)) & C != B & r2_hidden(k4_tarski(B,C),A) ) ) ) ) ), file(orders_1,d11_orders_1), [interesting(0.00)]). fof(t15_orders_2,theorem,( $true ), file(orders_2,t15_orders_2), [interesting(0.00)]). fof(d13_orders_1,definition,( ! [A] : ( v1_relat_1(A) => ! [B] : ( r8_orders_1(A,B) <=> ( r2_hidden(B,k3_relat_1(A)) & ! [C] : ( r2_hidden(C,k3_relat_1(A)) => ( C = B | r2_hidden(k4_tarski(C,B),A) ) ) ) ) ) ), file(orders_1,d13_orders_1), [interesting(0.00)]). fof(d14_orders_1,definition,( ! [A] : ( v1_relat_1(A) => ! [B] : ( r9_orders_1(A,B) <=> ( r2_hidden(B,k3_relat_1(A)) & ! [C] : ( r2_hidden(C,k3_relat_1(A)) => ( C = B | r2_hidden(k4_tarski(B,C),A) ) ) ) ) ) ), file(orders_1,d14_orders_1), [interesting(0.00)]). fof(d7_relat_1,definition,( ! [A] : ( v1_relat_1(A) => ! [B] : ( v1_relat_1(B) => ( B = k4_relat_1(A) <=> ! [C,D] : ( r2_hidden(k4_tarski(C,D),B) <=> r2_hidden(k4_tarski(D,C),A) ) ) ) ) ), file(relat_1,d7_relat_1), [interesting(0.00)]). fof(t29_relat_2,theorem,( ! [A] : ( v1_relat_1(A) => ( v1_relat_2(A) => ( k1_relat_1(A) = k1_relat_1(k4_relat_1(A)) & k2_relat_1(A) = k2_relat_1(k4_relat_1(A)) ) ) ) ), file(relat_2,t29_relat_2), [interesting(0.00)]). fof(d4_partfun1,definition,( ! [A,B,C] : ( m2_relset_1(C,A,B) => ( v1_partfun1(C,A,B) <=> k4_relset_1(A,B,C) = A ) ) ), file(partfun1,d4_partfun1), [interesting(0.00)]). fof(t27_relat_2,theorem,( ! [A] : ( v1_relat_1(A) => ( v1_relat_2(A) => v1_relat_2(k4_relat_1(A)) ) ) ), file(relat_2,t27_relat_2), [interesting(0.00)]). fof(t40_relat_2,theorem,( ! [A] : ( v1_relat_1(A) => ( v4_relat_2(A) => v4_relat_2(k4_relat_1(A)) ) ) ), file(relat_2,t40_relat_2), [interesting(0.00)]). fof(t42_relat_2,theorem,( ! [A] : ( v1_relat_1(A) => ( v8_relat_2(A) => v8_relat_2(k4_relat_1(A)) ) ) ), file(relat_2,t42_relat_2), [interesting(0.00)]). fof(d1_struct_0,definition,( ! [A] : ( l1_struct_0(A) => ( v3_struct_0(A) <=> v1_xboole_0(u1_struct_0(A)) ) ) ), file(struct_0,d1_struct_0), [interesting(0.00)]). fof(d2_tarski,definition,( ! [A,B,C] : ( C = k2_tarski(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ( D = A | D = B ) ) ) ), file(tarski,d2_tarski), [interesting(0.00)]). fof(t36_orders_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & l1_orders_2(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( ( v5_orders_2(k2_struct_0(A,B,C),A) & m1_subset_1(k2_struct_0(A,B,C),k1_zfmisc_1(u1_struct_0(A))) ) <=> ( r3_orders_2(A,B,C) | r3_orders_2(A,C,B) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_tarski,d11_orders_2,d7_relat_2,d9_orders_2,d7_relat_2,d11_orders_2,d9_orders_2,d9_orders_2,d9_orders_2,d9_orders_2,d2_tarski]), [file(orders_2,t36_orders_2),interesting(0.00)]). fof(t38_orders_2,theorem,( ! [A] : ( ( v2_orders_2(A) & l1_orders_2(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( ~ ( ? [D] : ( v5_orders_2(D,A) & m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) & r2_hidden(B,D) & r2_hidden(C,D) ) & ~ r1_orders_2(A,B,C) & ~ r1_orders_2(A,C,B) ) & ~ ( ( r1_orders_2(A,B,C) | r1_orders_2(A,C,B) ) & ! [D] : ( ( v5_orders_2(D,A) & m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) ) => ~ ( r2_hidden(B,D) & r2_hidden(C,D) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d11_orders_2,d7_relat_2,d9_orders_2,d9_orders_2,t106_zfmisc_1,d1_struct_0,t36_orders_2,d2_tarski]), [file(orders_2,t38_orders_2),interesting(0.00)]). fof(d17_orders_2,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & v3_orders_2(A) & v4_orders_2(A) & l1_orders_2(A) ) => ! [B] : ( m1_orders_1(B,k1_orders_1(u1_struct_0(A))) => ! [C] : ( C = k4_orders_2(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> m2_orders_2(D,A,B) ) ) ) ) ), file(orders_2,d17_orders_2), [interesting(0.00)]). fof(t94_zfmisc_1,theorem,( ! [A,B] : ( ! [C] : ( r2_hidden(C,A) => r1_tarski(C,B) ) => r1_tarski(k3_tarski(A),B) ) ), file(zfmisc_1,t94_zfmisc_1), [interesting(0.00)]). fof(d4_tarski,definition,( ! [A,B] : ( B = k3_tarski(A) <=> ! [C] : ( r2_hidden(C,B) <=> ? [D] : ( r2_hidden(C,D) & r2_hidden(D,A) ) ) ) ), file(tarski,d4_tarski), [interesting(0.00)]). fof(d8_xboole_0,definition,( ! [A,B] : ( r2_xboole_0(A,B) <=> ( r1_tarski(A,B) & A != B ) ) ), file(xboole_0,d8_xboole_0), [interesting(0.00)]). fof(d16_orders_2,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & v3_orders_2(A) & v4_orders_2(A) & l1_orders_2(A) ) => ! [B] : ( m1_orders_1(B,k1_orders_1(u1_struct_0(A))) => ! [C] : ( ( v5_orders_2(C,A) & m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) ) => ( m2_orders_2(C,A,B) <=> ( C != k1_xboole_0 & r2_wellord1(u1_orders_2(A),C) & ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( r2_hidden(D,C) => k1_funct_1(B,k1_orders_2(A,k3_orders_2(A,C,D))) = D ) ) ) ) ) ) ) ), file(orders_2,d16_orders_2), [interesting(0.00)]). fof(d15_orders_2,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & v3_orders_2(A) & v4_orders_2(A) & l1_orders_2(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ( ( B != k1_xboole_0 => ( m1_orders_2(C,A,B) <=> ? [D] : ( m1_subset_1(D,u1_struct_0(A)) & r2_hidden(D,B) & C = k3_orders_2(A,B,D) ) ) ) & ( B = k1_xboole_0 => ( m1_orders_2(C,A,B) <=> C = k1_xboole_0 ) ) ) ) ) ) ), file(orders_2,d15_orders_2), [interesting(0.00)]). fof(t17_xboole_1,theorem,( ! [A,B] : r1_tarski(k3_xboole_0(A,B),A) ), file(xboole_1,t17_xboole_1), [interesting(0.00)]). fof(d3_xboole_0,definition,( ! [A,B,C] : ( C = k3_xboole_0(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ( r2_hidden(D,A) & r2_hidden(D,B) ) ) ) ), file(xboole_0,d3_xboole_0), [interesting(0.00)]). fof(t1_xboole_1,theorem,( ! [A,B,C] : ( ( r1_tarski(A,B) & r1_tarski(B,C) ) => r1_tarski(A,C) ) ), file(xboole_1,t1_xboole_1), [interesting(0.00)]). fof(d1_tarski,definition,( ! [A,B] : ( B = k1_tarski(A) <=> ! [C] : ( r2_hidden(C,B) <=> C = A ) ) ), file(tarski,d1_tarski), [interesting(0.00)]). fof(t57_orders_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & v3_orders_2(A) & v4_orders_2(A) & l1_orders_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,k1_zfmisc_1(u1_struct_0(A))) => ( r2_hidden(B,k3_orders_2(A,D,C)) <=> ( r2_orders_2(A,B,C) & r2_hidden(B,D) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t56_orders_2,t52_orders_2]), [file(orders_2,t57_orders_2),interesting(0.00)]). fof(d8_relat_2,definition,( ! [A] : ( v1_relat_1(A) => ! [B] : ( r8_relat_2(A,B) <=> ! [C,D,E] : ( ( r2_hidden(C,B) & r2_hidden(D,B) & r2_hidden(E,B) & r2_hidden(k4_tarski(C,D),A) & r2_hidden(k4_tarski(D,E),A) ) => r2_hidden(k4_tarski(C,E),A) ) ) ) ), file(relat_2,d8_relat_2), [interesting(0.00)]). fof(d4_relat_2,definition,( ! [A] : ( v1_relat_1(A) => ! [B] : ( r4_relat_2(A,B) <=> ! [C,D] : ( ( r2_hidden(C,B) & r2_hidden(D,B) & r2_hidden(k4_tarski(C,D),A) & r2_hidden(k4_tarski(D,C),A) ) => C = D ) ) ) ), file(relat_2,d4_relat_2), [interesting(0.00)]). fof(t69_orders_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & v3_orders_2(A) & v4_orders_2(A) & l1_orders_2(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ~ ( ~ ( B = k1_xboole_0 & C = k1_xboole_0 ) & m1_orders_2(B,A,C) & m1_orders_2(C,A,B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d15_orders_2,d15_orders_2,d15_orders_2,d15_orders_2,d3_xboole_0,d1_tarski,t28_orders_2]), [file(orders_2,t69_orders_2),interesting(0.00)]). fof(t36_xboole_1,theorem,( ! [A,B] : r1_tarski(k4_xboole_0(A,B),A) ), file(xboole_1,t36_xboole_1), [interesting(0.00)]). fof(t37_xboole_1,theorem,( ! [A,B] : ( k4_xboole_0(A,B) = k1_xboole_0 <=> r1_tarski(A,B) ) ), file(xboole_1,t37_xboole_1), [interesting(0.00)]). fof(t9_wellord1,theorem,( ! [A,B] : ( v1_relat_1(B) => ( r2_wellord1(B,A) => ! [C] : ~ ( r1_tarski(C,A) & C != k1_xboole_0 & ! [D] : ~ ( r2_hidden(D,C) & ! [E] : ( r2_hidden(E,C) => r2_hidden(k4_tarski(D,E),B) ) ) ) ) ) ), file(wellord1,t9_wellord1), [interesting(0.00)]). fof(d4_xboole_0,definition,( ! [A,B,C] : ( C = k4_xboole_0(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ( r2_hidden(D,A) & ~ r2_hidden(D,B) ) ) ) ), file(xboole_0,d4_xboole_0), [interesting(0.00)]). fof(d5_wellord1,definition,( ! [A] : ( v1_relat_1(A) => ! [B] : ( r2_wellord1(A,B) <=> ( r1_relat_2(A,B) & r8_relat_2(A,B) & r4_relat_2(A,B) & r6_relat_2(A,B) & r1_wellord1(A,B) ) ) ) ), file(wellord1,d5_wellord1), [interesting(0.00)]). fof(t39_orders_2,theorem,( ! [A] : ( ( v2_orders_2(A) & v4_orders_2(A) & l1_orders_2(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( ? [D] : ( v5_orders_2(D,A) & m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) & r2_hidden(B,D) & r2_hidden(C,D) ) <=> ( r2_orders_2(A,B,C) <=> ~ r1_orders_2(A,C,B) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t30_orders_2,d10_orders_2,t38_orders_2,d10_orders_2,t38_orders_2]), [file(orders_2,t39_orders_2),interesting(0.00)]). fof(t3_xboole_1,theorem,( ! [A] : ( r1_tarski(A,k1_xboole_0) => A = k1_xboole_0 ) ), file(xboole_1,t3_xboole_1), [interesting(0.00)]). fof(t49_orders_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & v3_orders_2(A) & v4_orders_2(A) & l1_orders_2(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ~ ( r2_hidden(B,C) & r2_hidden(B,k2_orders_2(A,C)) ) ) ) ) ), file(orders_2,t49_orders_2), [interesting(0.00)]). fof(t4_orders_1,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ~ r2_hidden(k1_xboole_0,k1_orders_1(A)) ) ), file(orders_1,t4_orders_1), [interesting(0.00)]). fof(t5_orders_1,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ( r1_tarski(A,B) <=> r2_hidden(A,k1_orders_1(B)) ) ) ) ), file(orders_1,t5_orders_1), [interesting(0.00)]). fof(d1_orders_1,definition,( ! [A] : ( ~ v1_xboole_0(A) => ( ~ r2_hidden(k1_xboole_0,A) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,A,k3_tarski(A)) & m2_relset_1(B,A,k3_tarski(A)) ) => ( m1_orders_1(B,A) <=> ! [C] : ( r2_hidden(C,A) => r2_hidden(k1_funct_1(B,C),C) ) ) ) ) ) ), file(orders_1,d1_orders_1), [interesting(0.00)]). fof(d3_wellord1,definition,( ! [A] : ( v1_relat_1(A) => ! [B] : ( r1_wellord1(A,B) <=> ! [C] : ~ ( r1_tarski(C,B) & C != k1_xboole_0 & ! [D] : ~ ( r2_hidden(D,C) & r1_xboole_0(k1_wellord1(A,D),C) ) ) ) ) ), file(wellord1,d3_wellord1), [interesting(0.00)]). fof(t39_zfmisc_1,theorem,( ! [A,B] : ( r1_tarski(A,k1_tarski(B)) <=> ( A = k1_xboole_0 | A = k1_tarski(B) ) ) ), file(zfmisc_1,t39_zfmisc_1), [interesting(0.00)]). fof(d1_wellord1,definition,( ! [A] : ( v1_relat_1(A) => ! [B,C] : ( C = k1_wellord1(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ( D != B & r2_hidden(k4_tarski(D,B),A) ) ) ) ) ), file(wellord1,d1_wellord1), [interesting(0.00)]). fof(d7_xboole_0,definition,( ! [A,B] : ( r1_xboole_0(A,B) <=> k3_xboole_0(A,B) = k1_xboole_0 ) ), file(xboole_0,d7_xboole_0), [interesting(0.00)]). fof(t2_xboole_1,theorem,( ! [A] : r1_tarski(k1_xboole_0,A) ), file(xboole_1,t2_xboole_1), [interesting(0.00)]). fof(t91_orders_1,theorem,( ! [A] : ( ~ ( ? [B] : ( B != k1_xboole_0 & r2_hidden(B,A) ) & k3_tarski(A) = k1_xboole_0 ) & ~ ( k3_tarski(A) != k1_xboole_0 & ! [B] : ~ ( B != k1_xboole_0 & r2_hidden(B,A) ) ) ) ), file(orders_1,t91_orders_1), [interesting(0.00)]). fof(t92_zfmisc_1,theorem,( ! [A,B] : ( r2_hidden(A,B) => r1_tarski(A,k3_tarski(B)) ) ), file(zfmisc_1,t92_zfmisc_1), [interesting(0.00)]). fof(t70_orders_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & v3_orders_2(A) & v4_orders_2(A) & l1_orders_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,k1_zfmisc_1(u1_struct_0(A))) => ! [E] : ( m1_subset_1(E,k1_zfmisc_1(u1_struct_0(A))) => ( ( r2_orders_2(A,B,C) & r2_hidden(B,D) & r2_hidden(C,E) & m1_orders_2(E,A,D) ) => r2_hidden(B,E) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d15_orders_2,d1_tarski,d3_xboole_0,d1_tarski,t29_orders_2,d3_xboole_0]), [file(orders_2,t70_orders_2),interesting(0.00)]). fof(t3_xboole_0,theorem,( ! [A,B] : ( ~ ( ~ r1_xboole_0(A,B) & ! [C] : ~ ( r2_hidden(C,A) & r2_hidden(C,B) ) ) & ~ ( ? [C] : ( r2_hidden(C,A) & r2_hidden(C,B) ) & r1_xboole_0(A,B) ) ) ), file(xboole_0,t3_xboole_0), [interesting(0.00)]). fof(t37_zfmisc_1,theorem,( ! [A,B] : ( r1_tarski(k1_tarski(A),B) <=> r2_hidden(A,B) ) ), file(zfmisc_1,t37_zfmisc_1), [interesting(0.00)]). fof(t45_xboole_1,theorem,( ! [A,B] : ( r1_tarski(A,B) => B = k2_xboole_0(A,k4_xboole_0(B,A)) ) ), file(xboole_1,t45_xboole_1), [interesting(0.00)]). fof(t23_xboole_1,theorem,( ! [A,B,C] : k3_xboole_0(A,k2_xboole_0(B,C)) = k2_xboole_0(k3_xboole_0(A,B),k3_xboole_0(A,C)) ), file(xboole_1,t23_xboole_1), [interesting(0.00)]). fof(t56_zfmisc_1,theorem,( ! [A,B] : ( ~ r2_hidden(A,B) => r1_xboole_0(k1_tarski(A),B) ) ), file(zfmisc_1,t56_zfmisc_1), [interesting(0.00)]). fof(t83_xboole_1,theorem,( ! [A,B] : ( r1_xboole_0(A,B) <=> k4_xboole_0(A,B) = A ) ), file(xboole_1,t83_xboole_1), [interesting(0.00)]). fof(t7_xboole_1,theorem,( ! [A,B] : r1_tarski(A,k2_xboole_0(A,B)) ), file(xboole_1,t7_xboole_1), [interesting(0.00)]). fof(t65_orders_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & v3_orders_2(A) & v4_orders_2(A) & l1_orders_2(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) => ( r1_tarski(C,D) => r1_tarski(k3_orders_2(A,C,B),k3_orders_2(A,D,B)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,d3_xboole_0,d3_xboole_0,d3_xboole_0]), [file(orders_2,t65_orders_2),interesting(0.00)]). fof(t16_orders_2,theorem,( $true ), file(orders_2,t16_orders_2), [interesting(0.00)]). fof(t17_orders_2,theorem,( $true ), file(orders_2,t17_orders_2), [interesting(0.00)]). fof(t18_orders_2,theorem,( $true ), file(orders_2,t18_orders_2), [interesting(0.00)]). fof(t19_orders_2,theorem,( $true ), file(orders_2,t19_orders_2), [interesting(0.00)]). fof(t1_orders_2,theorem,( $true ), file(orders_2,t1_orders_2), [interesting(0.00)]). fof(t20_orders_2,theorem,( $true ), file(orders_2,t20_orders_2), [interesting(0.00)]). fof(t21_orders_2,theorem,( $true ), file(orders_2,t21_orders_2), [interesting(0.00)]). fof(t22_orders_2,theorem,( $true ), file(orders_2,t22_orders_2), [interesting(0.00)]). fof(t23_orders_2,theorem,( $true ), file(orders_2,t23_orders_2), [interesting(0.00)]). fof(t27_orders_2,theorem,( $true ), file(orders_2,t27_orders_2), [interesting(0.00)]). fof(t2_orders_2,theorem,( $true ), file(orders_2,t2_orders_2), [interesting(0.00)]). fof(t31_orders_2,theorem,( $true ), file(orders_2,t31_orders_2), [interesting(0.00)]). fof(t33_orders_2,theorem,( $true ), file(orders_2,t33_orders_2), [interesting(0.00)]). fof(t34_orders_2,theorem,( $true ), file(orders_2,t34_orders_2), [interesting(0.00)]). fof(t96_orders_1,theorem,( ! [A,B,C] : ( v1_relat_1(C) => ( ( r7_relat_2(C,A) & r1_tarski(B,A) ) => r7_relat_2(C,B) ) ) ), file(orders_1,t96_orders_1), [interesting(0.00)]). fof(t3_orders_2,theorem,( $true ), file(orders_2,t3_orders_2), [interesting(0.00)]). fof(t41_orders_2,theorem,( $true ), file(orders_2,t41_orders_2), [interesting(0.00)]). fof(t42_orders_2,theorem,( $true ), file(orders_2,t42_orders_2), [interesting(0.00)]). fof(t12_pre_topc,theorem,( ! [A] : ( l1_struct_0(A) => k2_pre_topc(A) = u1_struct_0(A) ) ), file(pre_topc,t12_pre_topc), [interesting(0.00)]). fof(t47_orders_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & v3_orders_2(A) & v4_orders_2(A) & l1_orders_2(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ~ ( r2_hidden(B,C) & r2_hidden(B,k1_orders_2(A,C)) ) ) ) ) ), file(orders_2,t47_orders_2), [interesting(0.00)]). fof(t4_orders_2,theorem,( $true ), file(orders_2,t4_orders_2), [interesting(0.00)]). fof(t53_orders_2,theorem,( $true ), file(orders_2,t53_orders_2), [interesting(0.00)]). fof(t54_orders_2,theorem,( $true ), file(orders_2,t54_orders_2), [interesting(0.00)]). fof(t55_orders_2,theorem,( $true ), file(orders_2,t55_orders_2), [interesting(0.00)]). fof(t58_orders_2,theorem,( $true ), file(orders_2,t58_orders_2), [interesting(0.00)]). fof(t59_orders_2,theorem,( $true ), file(orders_2,t59_orders_2), [interesting(0.00)]). fof(t5_orders_2,theorem,( $true ), file(orders_2,t5_orders_2), [interesting(0.00)]). fof(t60_orders_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & v3_orders_2(A) & v4_orders_2(A) & l1_orders_2(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k3_orders_2(A,k1_pre_topc(A),B) = k1_xboole_0 ) ) ), file(orders_2,t60_orders_2), [interesting(0.00)]). fof(t63_orders_2,theorem,( $true ), file(orders_2,t63_orders_2), [interesting(0.00)]). fof(t64_orders_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & v3_orders_2(A) & v4_orders_2(A) & l1_orders_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,k1_zfmisc_1(u1_struct_0(A))) => ( r2_orders_2(A,B,C) => r1_tarski(k3_orders_2(A,D,B),k3_orders_2(A,D,C)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,d3_xboole_0,d3_xboole_0,d1_tarski,t29_orders_2,d1_tarski,d3_xboole_0]), [file(orders_2,t64_orders_2),interesting(0.00)]). fof(t66_orders_2,theorem,( $true ), file(orders_2,t66_orders_2), [interesting(0.00)]). fof(t6_orders_2,theorem,( $true ), file(orders_2,t6_orders_2), [interesting(0.00)]). fof(t72_orders_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_orders_2(A) & v3_orders_2(A) & v4_orders_2(A) & l1_orders_2(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ~ ( r1_tarski(B,C) & r2_wellord1(u1_orders_2(A),C) & ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ( ( r2_hidden(E,B) & r2_orders_2(A,D,E) ) => r2_hidden(D,B) ) ) ) & B != C & ~ m1_orders_2(B,A,C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d10_xboole_0,t36_xboole_1,t37_xboole_1,t9_wellord1,d4_xboole_0,d3_tarski,t40_orders_2,d1_tarski,t39_orders_2,d4_xboole_0,d10_orders_2,d4_xboole_0,d3_xboole_0,d10_xboole_0,d3_tarski,d3_xboole_0,d9_orders_2,d1_tarski,t30_orders_2,d3_xboole_0,d4_xboole_0,t3_xboole_1,d15_orders_2]), [file(orders_2,t72_orders_2),interesting(0.00)]). fof(t74_orders_2,theorem,( $true ), file(orders_2,t74_orders_2), [interesting(0.00)]). fof(t75_orders_2,theorem,( $true ), file(orders_2,t75_orders_2), [interesting(0.00)]). fof(t76_orders_2,theorem,( $true ), file(orders_2,t76_orders_2), [interesting(0.00)]). fof(t77_orders_2,theorem,( $true ), file(orders_2,t77_orders_2), [interesting(0.00)]). fof(t7_orders_2,theorem,( $true ), file(orders_2,t7_orders_2), [interesting(0.00)]). fof(l7_orders_2,theorem,( ! [A,B] : ( ( ~ v3_struct_0(B) & v2_orders_2(B) & v3_orders_2(B) & v4_orders_2(B) & l1_orders_2(B) ) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B))) => ( r2_hidden(A,C) => m1_subset_1(A,u1_struct_0(B)) ) ) ) ), file(orders_2,l7_orders_2), [interesting(0.00)]). fof(t85_orders_2,theorem,( $true ), file(orders_2,t85_orders_2), [interesting(0.00)]). fof(t86_orders_2,theorem,( $true ), file(orders_2,t86_orders_2), [interesting(0.00)]). fof(t8_orders_2,theorem,( $true ), file(orders_2,t8_orders_2), [interesting(0.00)]). fof(t90_orders_2,theorem,( $true ), file(orders_2,t90_orders_2), [interesting(0.00)]). fof(t91_orders_2,theorem,( $true ), file(orders_2,t91_orders_2), [interesting(0.00)]). fof(t92_orders_2,theorem,( $true ), file(orders_2,t92_orders_2), [interesting(0.00)]). fof(t93_orders_2,theorem,( $true ), file(orders_2,t93_orders_2), [interesting(0.00)]). fof(t94_orders_2,theorem,( $true ), file(orders_2,t94_orders_2), [interesting(0.00)]). fof(t95_orders_2,theorem,( $true ), file(orders_2,t95_orders_2), [interesting(0.00)]). fof(t96_orders_2,theorem,( $true ), file(orders_2,t96_orders_2), [interesting(0.00)]). fof(t97_orders_2,theorem,( $true ), file(orders_2,t97_orders_2), [interesting(0.00)]). fof(t98_orders_2,theorem,( $true ), file(orders_2,t98_orders_2), [interesting(0.00)]). fof(t99_orders_2,theorem,( $true ), file(orders_2,t99_orders_2), [interesting(0.00)]). fof(t9_orders_2,theorem,( $true ), file(orders_2,t9_orders_2), [interesting(0.00)]).