% Mizar problem: t45_simplex0,simplex0,2811,6 include('/home/mptp/mizwrk/7.13.01_4.181.1147/MPTP2/pl/../AxiomsThf/SET010^0.ax'). thf(n0_type, type, 0: $i). thf(n1_type, type, 1: $i). thf(n2_type, type, 2: $i). thf(g1_pre_topc_type, type, g1_pre_topc: $i > $i > $i). thf(k1_card_1_type, type, k1_card_1: $i > $i). thf(k1_matroid0_type, type, k1_matroid0: $i > $i). thf(k1_numbers_type, type, k1_numbers: $i). thf(k1_simplex0_type, type, k1_simplex0: $i > $i). thf(k1_xboole_0_type, type, k1_xboole_0: $i). thf(k1_xxreal_3_type, type, k1_xxreal_3: $i > $i > $i). thf(k1_zfmisc_1_type, type, k1_zfmisc_1: $i > $i). thf(k2_simplex0_type, type, k2_simplex0: $i > $i > $i). thf(k2_xcmplx_0_type, type, k2_xcmplx_0: $i > $i > $i). thf(k2_xxreal_3_type, type, k2_xxreal_3: $i > $i). thf(k3_simplex0_type, type, k3_simplex0: $i > $i > $i > $i). thf(k4_ordinal1_type, type, k4_ordinal1: $i). thf(k4_xcmplx_0_type, type, k4_xcmplx_0: $i > $i). thf(k5_card_1_type, type, k5_card_1: $i > $i). thf(k5_numbers_type, type, k5_numbers: $i). thf(k5_simplex0_type, type, k5_simplex0: $i > $i > $i). thf(k6_numbers_type, type, k6_numbers: $i). thf(k6_simplex0_type, type, k6_simplex0: $i > $i). thf(k6_xcmplx_0_type, type, k6_xcmplx_0: $i > $i > $i). thf(k7_xcmplx_0_type, type, k7_xcmplx_0: $i > $i > $i). thf(k8_simplex0_type, type, k8_simplex0: $i > $i > $i > $i). thf(u1_pre_topc_type, type, u1_pre_topc: $i > $i). thf(u1_struct_0_type, type, u1_struct_0: $i > $i). thf(l1_pre_topc_type, type, l1_pre_topc: $i > $o). thf(l1_struct_0_type, type, l1_struct_0: $i > $o). thf(m1_simplex0_type, type, m1_simplex0: $i > $i > $o). thf(m1_subset_1_type, type, m1_subset_1: $i > $i > $o). thf(m2_subset_1_type, type, m2_subset_1: $i > $i > $i > $o). thf(r1_ordinal1_type, type, r1_ordinal1: $i > $i > $o). thf(r1_tarski_type, type, r1_tarski: $i > $i > $o). thf(r1_xxreal_0_type, type, r1_xxreal_0: $i > $i > $o). thf(v13_struct_0_type, type, v13_struct_0: $i > $i > $o). thf(v1_card_1_type, type, v1_card_1: $i > $o). thf(v1_classes1_type, type, v1_classes1: $i > $o). thf(v1_coh_sp_type, type, v1_coh_sp: $i > $o). thf(v1_finset_1_type, type, v1_finset_1: $i > $o). thf(v1_funcop_1_type, type, v1_funcop_1: $i > $o). thf(v1_funct_1_type, type, v1_funct_1: $i > $o). thf(v1_int_1_type, type, v1_int_1: $i > $o). thf(v1_matroid0_type, type, v1_matroid0: $i > $o). thf(v1_ordinal1_type, type, v1_ordinal1: $i > $o). thf(v1_pre_topc_type, type, v1_pre_topc: $i > $o). thf(v1_relat_1_type, type, v1_relat_1: $i > $o). thf(v1_setfam_1_type, type, v1_setfam_1: $i > $o). thf(v1_subset_1_type, type, v1_subset_1: $i > $i > $o). thf(v1_xboole_0_type, type, v1_xboole_0: $i > $o). thf(v1_xcmplx_0_type, type, v1_xcmplx_0: $i > $o). thf(v1_xreal_0_type, type, v1_xreal_0: $i > $o). thf(v1_xxreal_0_type, type, v1_xxreal_0: $i > $o). thf(v1_zfmisc_1_type, type, v1_zfmisc_1: $i > $o). thf(v2_card_1_type, type, v2_card_1: $i > $o). thf(v2_finset_1_type, type, v2_finset_1: $i > $o). thf(v2_finsub_1_type, type, v2_finsub_1: $i > $o). thf(v2_funcop_1_type, type, v2_funcop_1: $i > $o). thf(v2_funct_1_type, type, v2_funct_1: $i > $o). thf(v2_ordinal1_type, type, v2_ordinal1: $i > $o). thf(v2_relat_1_type, type, v2_relat_1: $i > $o). thf(v2_setfam_1_type, type, v2_setfam_1: $i > $o). thf(v2_simplex0_type, type, v2_simplex0: $i > $o). thf(v2_struct_0_type, type, v2_struct_0: $i > $o). thf(v2_xxreal_0_type, type, v2_xxreal_0: $i > $o). thf(v3_card_1_type, type, v3_card_1: $i > $i > $o). thf(v3_cohsp_1_type, type, v3_cohsp_1: $i > $o). thf(v3_funct_1_type, type, v3_funct_1: $i > $o). thf(v3_matroid0_type, type, v3_matroid0: $i > $o). thf(v3_ordinal1_type, type, v3_ordinal1: $i > $o). thf(v3_pencil_1_type, type, v3_pencil_1: $i > $o). thf(v3_pre_topc_type, type, v3_pre_topc: $i > $i > $o). thf(v3_relat_1_type, type, v3_relat_1: $i > $o). thf(v3_simplex0_type, type, v3_simplex0: $i > $o). thf(v3_xxreal_0_type, type, v3_xxreal_0: $i > $o). thf(v3_xxreal_2_type, type, v3_xxreal_2: $i > $o). thf(v4_funct_1_type, type, v4_funct_1: $i > $o). thf(v4_matroid0_type, type, v4_matroid0: $i > $o). thf(v4_simplex0_type, type, v4_simplex0: $i > $o). thf(v5_finset_1_type, type, v5_finset_1: $i > $o). thf(v5_ordinal1_type, type, v5_ordinal1: $i > $o). thf(v5_simplex0_type, type, v5_simplex0: $i > $o). thf(v6_ordinal1_type, type, v6_ordinal1: $i > $o). thf(v6_pre_topc_type, type, v6_pre_topc: $i > $o). thf(v6_simplex0_type, type, v6_simplex0: $i > $i > $o). thf(v7_ordinal1_type, type, v7_ordinal1: $i > $o). thf(v7_struct_0_type, type, v7_struct_0: $i > $o). thf(v8_struct_0_type, type, v8_struct_0: $i > $o). thf(abstractness_v1_pre_topc, axiom, (! [A: $i] : ( (l1_pre_topc @ A) => ( (v1_pre_topc @ A) => ( (= @ A) @ ( (g1_pre_topc @ (u1_struct_0 @ A) ) @ (u1_pre_topc @ A) ) ) ) ) ) , file(pre_topc, v1_pre_topc)). thf(antisymmetry_r2_hidden, axiom, (! [A: $i, B: $i] : ( ( (r2_hidden @ A) @ B) => ~ ( ( (r2_hidden @ B) @ A) ) ) ) , file(hidden, r2_hidden)). thf(cc10_card_1, axiom, (! [A: $i] : ( ( ~ ( (v1_xboole_0 @ A) ) & (v1_zfmisc_1 @ A) ) => ( (v3_card_1 @ A) @ 1) ) ) , file(card_1, cc10_card_1)). thf(cc10_ordinal1, axiom, (! [A: $i] : ( (v6_ordinal1 @ A) => (! [B: $i] : ( ( (m1_subset_1 @ B) @ (k1_zfmisc_1 @ A) ) => (v6_ordinal1 @ B) ) ) ) ) , file(ordinal1, cc10_ordinal1)). thf(cc10_simplex0, axiom, (! [A: $i] : ( (l1_pre_topc @ A) => ( ( (v1_matroid0 @ A) & (v3_simplex0 @ A) ) => (v3_matroid0 @ A) ) ) ) , file(simplex0, cc10_simplex0)). thf(cc10_struct_0, axiom, (! [A: $i] : ( (l1_struct_0 @ A) => ( ( ~ ( (v2_struct_0 @ A) ) & (v7_struct_0 @ A) ) => ( (v13_struct_0 @ A) @ 1) ) ) ) , file(struct_0, cc10_struct_0)). thf(cc11_struct_0, axiom, (! [A: $i] : ( (l1_struct_0 @ A) => ( ( (v13_struct_0 @ A) @ 1) => ( ~ ( (v2_struct_0 @ A) ) & (v7_struct_0 @ A) ) ) ) ) , file(struct_0, cc11_struct_0)). thf(cc13_simplex0, axiom, (! [A: $i] : ( ( ~ ( (v5_simplex0 @ A) ) & (l1_pre_topc @ A) ) => (! [B: $i] : ( ( (m1_subset_1 @ B) @ (k1_zfmisc_1 @ (u1_struct_0 @ A) ) ) => ( (v1_xboole_0 @ B) => ( (v3_pre_topc @ B) @ A) ) ) ) ) ) , file(simplex0, cc13_simplex0)). thf(cc17_simplex0, axiom, (! [A: $i] : ( (v1_int_1 @ A) => ( (v1_finset_1 @ A) & (v1_int_1 @ A) ) ) ) , file(simplex0, cc17_simplex0)). thf(cc17_struct_0, axiom, (! [A: $i] : ( (l1_struct_0 @ A) => ( ~ ( (v7_struct_0 @ A) ) => ~ ( (v2_struct_0 @ A) ) ) ) ) , file(struct_0, cc17_struct_0)). thf(cc1_card_1, axiom, (! [A: $i] : ( (v1_card_1 @ A) => (v3_ordinal1 @ A) ) ) , file(card_1, cc1_card_1)). thf(cc1_fib_num2, axiom, (! [A: $i] : ( (v1_setfam_1 @ A) => (! [B: $i] : ( ( (m1_subset_1 @ B) @ (k1_zfmisc_1 @ A) ) => (v1_setfam_1 @ B) ) ) ) ) , file(fib_num2, cc1_fib_num2)). thf(cc1_finset_1, axiom, (! [A: $i] : ( (v1_xboole_0 @ A) => (v1_finset_1 @ A) ) ) , file(finset_1, cc1_finset_1)). thf(cc1_funct_1, axiom, (! [A: $i] : ( (v1_xboole_0 @ A) => (v1_funct_1 @ A) ) ) , file(funct_1, cc1_funct_1)). thf(cc1_matroid0, axiom, (! [A: $i] : ( ( ~ ( (v3_pencil_1 @ A) ) & ( (v1_matroid0 @ A) & (l1_pre_topc @ A) ) ) => (! [B: $i] : ( ( (m1_subset_1 @ B) @ (k1_zfmisc_1 @ (u1_struct_0 @ A) ) ) => ( (v1_xboole_0 @ B) => ( (v3_pre_topc @ B) @ A) ) ) ) ) ) , file(matroid0, cc1_matroid0)). thf(cc1_nat_1, axiom, (! [A: $i] : ( (v7_ordinal1 @ A) => ( (v3_ordinal1 @ A) & (v7_ordinal1 @ A) ) ) ) , file(nat_1, cc1_nat_1)). thf(cc1_ordinal1, axiom, (! [A: $i] : ( (v3_ordinal1 @ A) => ( (v1_ordinal1 @ A) & (v2_ordinal1 @ A) ) ) ) , file(ordinal1, cc1_ordinal1)). thf(cc1_relat_1, axiom, (! [A: $i] : ( (v1_xboole_0 @ A) => (v1_relat_1 @ A) ) ) , file(relat_1, cc1_relat_1)). thf(cc1_setfam_1, axiom, (! [A: $i] : ( ( ~ ( (v1_xboole_0 @ A) ) & (v1_setfam_1 @ A) ) => (! [B: $i] : ( ( (m1_subset_1 @ B) @ A) => ~ ( (v1_xboole_0 @ B) ) ) ) ) ) , file(setfam_1, cc1_setfam_1)). thf(cc1_simplex0, axiom, (! [A: $i] : ( (v1_xboole_0 @ A) => (v1_classes1 @ A) ) ) , file(simplex0, cc1_simplex0)). thf(cc1_struct_0, axiom, (! [A: $i] : ( (l1_struct_0 @ A) => ( (v2_struct_0 @ A) => (v7_struct_0 @ A) ) ) ) , file(struct_0, cc1_struct_0)). thf(cc1_subset_1, axiom, (! [A: $i] : ( (v1_xboole_0 @ A) => (! [B: $i] : ( ( (m1_subset_1 @ B) @ (k1_zfmisc_1 @ A) ) => (v1_xboole_0 @ B) ) ) ) ) , file(subset_1, cc1_subset_1)). thf(cc1_xreal_0, axiom, (! [A: $i] : ( ( (m1_subset_1 @ A) @ k1_numbers) => (v1_xreal_0 @ A) ) ) , file(xreal_0, cc1_xreal_0)). thf(cc1_xxreal_3, axiom, (! [A: $i] : ( ( (v1_xxreal_0 @ A) & ( ~ ( (v3_xxreal_0 @ A) ) & ~ ( (v1_xreal_0 @ A) ) ) ) => ( (v1_xxreal_0 @ A) & (v2_xxreal_0 @ A) ) ) ) , file(xxreal_3, cc1_xxreal_3)). thf(cc2_card_1, axiom, (! [A: $i] : ( (v1_xboole_0 @ A) => (v1_card_1 @ A) ) ) , file(card_1, cc2_card_1)). thf(cc2_finset_1, axiom, (! [A: $i] : ( (v1_finset_1 @ A) => (! [B: $i] : ( ( (m1_subset_1 @ B) @ (k1_zfmisc_1 @ A) ) => (v1_finset_1 @ B) ) ) ) ) , file(finset_1, cc2_finset_1)). thf(cc2_funcop_1, axiom, (! [A: $i] : ( ( (v1_relat_1 @ A) & ( (v1_funct_1 @ A) & (v1_funcop_1 @ A) ) ) => ( (v1_relat_1 @ A) & ( (v1_funct_1 @ A) & (v2_funcop_1 @ A) ) ) ) ) , file(funcop_1, cc2_funcop_1)). thf(cc2_funct_1, axiom, (! [A: $i] : ( ( (v1_xboole_0 @ A) & ( (v1_relat_1 @ A) & (v1_funct_1 @ A) ) ) => ( (v1_relat_1 @ A) & ( (v1_funct_1 @ A) & (v2_funct_1 @ A) ) ) ) ) , file(funct_1, cc2_funct_1)). thf(cc2_int_1, axiom, (! [A: $i] : ( (v7_ordinal1 @ A) => (v1_int_1 @ A) ) ) , file(int_1, cc2_int_1)). thf(cc2_matroid0, axiom, (! [A: $i] : ( (l1_pre_topc @ A) => ( (v4_matroid0 @ A) => (v3_matroid0 @ A) ) ) ) , file(matroid0, cc2_matroid0)). thf(cc2_nat_1, axiom, (! [A: $i] : ( ( (m1_subset_1 @ A) @ k5_numbers) => ~ ( (v3_xxreal_0 @ A) ) ) ) , file(nat_1, cc2_nat_1)). thf(cc2_ordinal1, axiom, (! [A: $i] : ( ( (v1_ordinal1 @ A) & (v2_ordinal1 @ A) ) => (v3_ordinal1 @ A) ) ) , file(ordinal1, cc2_ordinal1)). thf(cc2_relat_1, axiom, (! [A: $i] : ( (v1_relat_1 @ A) => (! [B: $i] : ( ( (m1_subset_1 @ B) @ (k1_zfmisc_1 @ A) ) => (v1_relat_1 @ B) ) ) ) ) , file(relat_1, cc2_relat_1)). thf(cc2_setfam_1, axiom, (! [A: $i] : ( ~ ( (v2_setfam_1 @ A) ) => ~ ( (v1_xboole_0 @ A) ) ) ) , file(setfam_1, cc2_setfam_1)). thf(cc2_simplex0, axiom, (! [A: $i] : ( ~ ( (v1_setfam_1 @ A) ) => ~ ( (v1_xboole_0 @ A) ) ) ) , file(simplex0, cc2_simplex0)). thf(cc2_struct_0, axiom, (! [A: $i] : ( (l1_struct_0 @ A) => ( ~ ( (v7_struct_0 @ A) ) => ~ ( (v2_struct_0 @ A) ) ) ) ) , file(struct_0, cc2_struct_0)). thf(cc2_subset_1, axiom, (! [A: $i] : ( ~ ( (v1_xboole_0 @ A) ) => (! [B: $i] : ( ( (m1_subset_1 @ B) @ (k1_zfmisc_1 @ A) ) => ( ~ ( ( (v1_subset_1 @ B) @ A) ) => ~ ( (v1_xboole_0 @ B) ) ) ) ) ) ) , file(subset_1, cc2_subset_1)). thf(cc2_xreal_0, axiom, (! [A: $i] : ( (v7_ordinal1 @ A) => (v1_xreal_0 @ A) ) ) , file(xreal_0, cc2_xreal_0)). thf(cc2_xxreal_0, axiom, (! [A: $i] : ( (v7_ordinal1 @ A) => (v1_xxreal_0 @ A) ) ) , file(xxreal_0, cc2_xxreal_0)). thf(cc2_xxreal_3, axiom, (! [A: $i] : ( ( (v1_xxreal_0 @ A) & ( ~ ( (v2_xxreal_0 @ A) ) & ~ ( (v1_xreal_0 @ A) ) ) ) => ( (v1_xxreal_0 @ A) & (v3_xxreal_0 @ A) ) ) ) , file(xxreal_3, cc2_xxreal_3)). thf(cc3_card_1, axiom, (! [A: $i] : ( (v7_ordinal1 @ A) => (v1_card_1 @ A) ) ) , file(card_1, cc3_card_1)). thf(cc3_cohsp_1, axiom, (! [A: $i] : ( (v1_classes1 @ A) => (v2_finsub_1 @ A) ) ) , file(cohsp_1, cc3_cohsp_1)). thf(cc3_funcop_1, axiom, (! [A: $i] : ( ( (v1_relat_1 @ A) & ( (v1_funct_1 @ A) & (v1_xboole_0 @ A) ) ) => ( (v1_relat_1 @ A) & ( (v1_funct_1 @ A) & (v1_funcop_1 @ A) ) ) ) ) , file(funcop_1, cc3_funcop_1)). thf(cc3_funct_1, axiom, (! [A: $i] : ( ( (v1_relat_1 @ A) & (v1_funct_1 @ A) ) => (! [B: $i] : ( ( (m1_subset_1 @ B) @ (k1_zfmisc_1 @ A) ) => (v1_funct_1 @ B) ) ) ) ) , file(funct_1, cc3_funct_1)). thf(cc3_int_1, axiom, (! [A: $i] : ( (v1_int_1 @ A) => (v1_xreal_0 @ A) ) ) , file(int_1, cc3_int_1)). thf(cc3_matroid0, axiom, (! [A: $i] : ( (l1_pre_topc @ A) => ( (v8_struct_0 @ A) => (v4_matroid0 @ A) ) ) ) , file(matroid0, cc3_matroid0)). thf(cc3_nat_1, axiom, (! [A: $i] : ( (v7_ordinal1 @ A) => ( (v7_ordinal1 @ A) & ~ ( (v3_xxreal_0 @ A) ) ) ) ) , file(nat_1, cc3_nat_1)). thf(cc3_ordinal1, axiom, (! [A: $i] : ( (v1_xboole_0 @ A) => (v3_ordinal1 @ A) ) ) , file(ordinal1, cc3_ordinal1)). thf(cc3_relat_1, axiom, (! [A: $i] : ( ( (v1_xboole_0 @ A) & (v1_relat_1 @ A) ) => ( (v1_relat_1 @ A) & (v3_relat_1 @ A) ) ) ) , file(relat_1, cc3_relat_1)). thf(cc3_setfam_1, axiom, (! [A: $i] : ( ( ~ ( (v1_xboole_0 @ A) ) & (v1_setfam_1 @ A) ) => ~ ( (v2_setfam_1 @ A) ) ) ) , file(setfam_1, cc3_setfam_1)). thf(cc3_simplex0, axiom, (! [A: $i] : ( ( ~ ( (v1_xboole_0 @ A) ) & (v1_classes1 @ A) ) => ~ ( (v1_setfam_1 @ A) ) ) ) , file(simplex0, cc3_simplex0)). thf(cc3_subset_1, axiom, (! [A: $i] : ( ~ ( (v1_xboole_0 @ A) ) => (! [B: $i] : ( ( (m1_subset_1 @ B) @ (k1_zfmisc_1 @ A) ) => ( (v1_xboole_0 @ B) => ( (v1_subset_1 @ B) @ A) ) ) ) ) ) , file(subset_1, cc3_subset_1)). thf(cc3_xreal_0, axiom, (! [A: $i] : ( (v1_xreal_0 @ A) => (v1_xcmplx_0 @ A) ) ) , file(xreal_0, cc3_xreal_0)). thf(cc3_xxreal_0, axiom, (! [A: $i] : ( ( (v1_xxreal_0 @ A) & (v2_xxreal_0 @ A) ) => ( ~ ( (v1_xboole_0 @ A) ) & ( (v1_xxreal_0 @ A) & ~ ( (v3_xxreal_0 @ A) ) ) ) ) ) , file(xxreal_0, cc3_xxreal_0)). thf(cc4_card_1, axiom, (! [A: $i] : ( ( (m1_subset_1 @ A) @ k4_ordinal1) => (v1_finset_1 @ A) ) ) , file(card_1, cc4_card_1)). thf(cc4_cohsp_1, axiom, (! [A: $i] : ( ( ~ ( (v1_xboole_0 @ A) ) & ( (v1_classes1 @ A) & (v1_coh_sp @ A) ) ) => ( ~ ( (v1_xboole_0 @ A) ) & ( (v1_classes1 @ A) & ( (v1_coh_sp @ A) & (v3_cohsp_1 @ A) ) ) ) ) ) , file(cohsp_1, cc4_cohsp_1)). thf(cc4_finset_1, axiom, (! [A: $i] : ( (v1_zfmisc_1 @ A) => (v1_finset_1 @ A) ) ) , file(finset_1, cc4_finset_1)). thf(cc4_funct_1, axiom, (! [A: $i] : ( ( (v1_xboole_0 @ A) & ( (v1_relat_1 @ A) & (v1_funct_1 @ A) ) ) => ( (v1_relat_1 @ A) & ( (v1_funct_1 @ A) & (v3_funct_1 @ A) ) ) ) ) , file(funct_1, cc4_funct_1)). thf(cc4_ordinal1, axiom, (! [A: $i] : ( (v1_xboole_0 @ A) => (v5_ordinal1 @ A) ) ) , file(ordinal1, cc4_ordinal1)). thf(cc4_relat_1, axiom, (! [A: $i] : ( ( (v1_xboole_0 @ A) & (v1_relat_1 @ A) ) => ( (v1_relat_1 @ A) & (v2_relat_1 @ A) ) ) ) , file(relat_1, cc4_relat_1)). thf(cc4_setfam_1, axiom, (! [A: $i] : ( ~ ( (v1_zfmisc_1 @ A) ) => ~ ( (v2_setfam_1 @ A) ) ) ) , file(setfam_1, cc4_setfam_1)). thf(cc4_simplex0, axiom, (! [A: $i] : ( (l1_pre_topc @ A) => ( ~ ( (v5_simplex0 @ A) ) => ~ ( (v3_pencil_1 @ A) ) ) ) ) , file(simplex0, cc4_simplex0)). thf(cc4_struct_0, axiom, (! [A: $i] : ( (l1_struct_0 @ A) => ( (v2_struct_0 @ A) => ( (v2_struct_0 @ A) & (v8_struct_0 @ A) ) ) ) ) , file(struct_0, cc4_struct_0)). thf(cc4_subset_1, axiom, (! [A: $i] : ( (v1_xboole_0 @ A) => (! [B: $i] : ( ( (m1_subset_1 @ B) @ (k1_zfmisc_1 @ A) ) => ~ ( ( (v1_subset_1 @ B) @ A) ) ) ) ) ) , file(subset_1, cc4_subset_1)). thf(cc4_xreal_0, axiom, (! [A: $i] : ( (v1_xreal_0 @ A) => (v1_xxreal_0 @ A) ) ) , file(xreal_0, cc4_xreal_0)). thf(cc4_xxreal_0, axiom, (! [A: $i] : ( ( ~ ( (v1_xboole_0 @ A) ) & ( (v1_xxreal_0 @ A) & ~ ( (v3_xxreal_0 @ A) ) ) ) => ( (v1_xxreal_0 @ A) & (v2_xxreal_0 @ A) ) ) ) , file(xxreal_0, cc4_xxreal_0)). thf(cc5_card_1, axiom, (! [A: $i] : ( (v7_ordinal1 @ A) => (v1_finset_1 @ A) ) ) , file(card_1, cc5_card_1)). thf(cc5_finset_1, axiom, (! [A: $i] : ( ~ ( (v1_finset_1 @ A) ) => ~ ( (v1_zfmisc_1 @ A) ) ) ) , file(finset_1, cc5_finset_1)). thf(cc5_funct_1, axiom, (! [A: $i] : ( ( (v1_relat_1 @ A) & ( (v1_funct_1 @ A) & ~ ( (v3_funct_1 @ A) ) ) ) => ( ~ ( (v1_zfmisc_1 @ A) ) & ( (v1_relat_1 @ A) & (v1_funct_1 @ A) ) ) ) ) , file(funct_1, cc5_funct_1)). thf(cc5_ordinal1, axiom, (! [A: $i] : ( (v3_ordinal1 @ A) => (! [B: $i] : ( ( (m1_subset_1 @ B) @ A) => (v3_ordinal1 @ B) ) ) ) ) , file(ordinal1, cc5_ordinal1)). thf(cc5_simplex0, axiom, (! [A: $i] : ( (l1_pre_topc @ A) => ( ~ ( (v4_simplex0 @ A) ) => ~ ( (v3_pencil_1 @ A) ) ) ) ) , file(simplex0, cc5_simplex0)). thf(cc5_struct_0, axiom, (! [A: $i] : ( (l1_struct_0 @ A) => ( ~ ( (v8_struct_0 @ A) ) => ( ~ ( (v2_struct_0 @ A) ) & ~ ( (v8_struct_0 @ A) ) ) ) ) ) , file(struct_0, cc5_struct_0)). thf(cc5_subset_1, axiom, (! [A: $i] : ( (v1_zfmisc_1 @ A) => (! [B: $i] : ( ( (m1_subset_1 @ B) @ (k1_zfmisc_1 @ A) ) => (v1_zfmisc_1 @ B) ) ) ) ) , file(subset_1, cc5_subset_1)). thf(cc5_xxreal_0, axiom, (! [A: $i] : ( ( (v1_xxreal_0 @ A) & (v3_xxreal_0 @ A) ) => ( ~ ( (v1_xboole_0 @ A) ) & ( (v1_xxreal_0 @ A) & ~ ( (v2_xxreal_0 @ A) ) ) ) ) ) , file(xxreal_0, cc5_xxreal_0)). thf(cc6_card_1, axiom, (! [A: $i] : ( ( (v3_ordinal1 @ A) & (v1_finset_1 @ A) ) => (v7_ordinal1 @ A) ) ) , file(card_1, cc6_card_1)). thf(cc6_finset_1, axiom, (! [A: $i] : ( (v1_xboole_0 @ A) => (v5_finset_1 @ A) ) ) , file(finset_1, cc6_finset_1)). thf(cc6_funct_1, axiom, (! [A: $i] : ( ( (v1_zfmisc_1 @ A) & ( (v1_relat_1 @ A) & (v1_funct_1 @ A) ) ) => ( (v1_relat_1 @ A) & ( (v1_funct_1 @ A) & (v3_funct_1 @ A) ) ) ) ) , file(funct_1, cc6_funct_1)). thf(cc6_matroid0, axiom, (! [A: $i] : ( ( ~ ( (v3_pencil_1 @ A) ) & ( (v3_matroid0 @ A) & (l1_pre_topc @ A) ) ) => (! [B: $i] : ( ( (m1_subset_1 @ B) @ (k1_zfmisc_1 @ (u1_struct_0 @ A) ) ) => ( ( (v3_pre_topc @ B) @ A) => ( (v1_finset_1 @ B) & ( (v3_pre_topc @ B) @ A) ) ) ) ) ) ) , file(matroid0, cc6_matroid0)). thf(cc6_ordinal1, axiom, (! [A: $i] : ( (v7_ordinal1 @ A) => (v3_ordinal1 @ A) ) ) , file(ordinal1, cc6_ordinal1)). thf(cc6_simplex0, axiom, (! [A: $i] : ( (l1_pre_topc @ A) => ( ( ~ ( (v3_pencil_1 @ A) ) & (v4_simplex0 @ A) ) => ~ ( (v5_simplex0 @ A) ) ) ) ) , file(simplex0, cc6_simplex0)). thf(cc6_struct_0, axiom, (! [A: $i] : ( (l1_struct_0 @ A) => ( (v7_struct_0 @ A) => (v8_struct_0 @ A) ) ) ) , file(struct_0, cc6_struct_0)). thf(cc6_xxreal_0, axiom, (! [A: $i] : ( ( ~ ( (v1_xboole_0 @ A) ) & ( (v1_xxreal_0 @ A) & ~ ( (v2_xxreal_0 @ A) ) ) ) => ( (v1_xxreal_0 @ A) & (v3_xxreal_0 @ A) ) ) ) , file(xxreal_0, cc6_xxreal_0)). thf(cc7_card_1, axiom, (! [A: $i] : ( ( (v3_card_1 @ A) @ k1_xboole_0) => (v1_xboole_0 @ A) ) ) , file(card_1, cc7_card_1)). thf(cc7_finset_1, axiom, (! [A: $i] : ( (v5_finset_1 @ A) => (! [B: $i] : ( ( (m1_subset_1 @ B) @ A) => (v1_finset_1 @ B) ) ) ) ) , file(finset_1, cc7_finset_1)). thf(cc7_funct_1, axiom, (! [A: $i] : ( (v1_xboole_0 @ A) => (v4_funct_1 @ A) ) ) , file(funct_1, cc7_funct_1)). thf(cc7_ordinal1, axiom, (! [A: $i] : ( (v1_xboole_0 @ A) => (v7_ordinal1 @ A) ) ) , file(ordinal1, cc7_ordinal1)). thf(cc7_simplex0, axiom, (! [A: $i] : ( (l1_pre_topc @ A) => ( ( ~ ( (v3_pencil_1 @ A) ) & (v1_matroid0 @ A) ) => ~ ( (v5_simplex0 @ A) ) ) ) ) , file(simplex0, cc7_simplex0)). thf(cc7_struct_0, axiom, (! [A: $i] : ( (l1_struct_0 @ A) => ( ~ ( (v8_struct_0 @ A) ) => ~ ( (v7_struct_0 @ A) ) ) ) ) , file(struct_0, cc7_struct_0)). thf(cc7_xxreal_0, axiom, (! [A: $i] : ( ( (v1_xboole_0 @ A) & (v1_xxreal_0 @ A) ) => ( (v1_xxreal_0 @ A) & ( ~ ( (v2_xxreal_0 @ A) ) & ~ ( (v3_xxreal_0 @ A) ) ) ) ) ) , file(xxreal_0, cc7_xxreal_0)). thf(cc8_card_1, axiom, (! [A: $i] : ( (v1_xboole_0 @ A) => ( (v3_card_1 @ A) @ k1_xboole_0) ) ) , file(card_1, cc8_card_1)). thf(cc8_finset_1, axiom, (! [A: $i] : ( (v5_finset_1 @ A) => (! [B: $i] : ( ( (m1_subset_1 @ B) @ (k1_zfmisc_1 @ A) ) => (v5_finset_1 @ B) ) ) ) ) , file(finset_1, cc8_finset_1)). thf(cc8_funct_1, axiom, (! [A: $i] : ( (v4_funct_1 @ A) => (! [B: $i] : ( ( (m1_subset_1 @ B) @ A) => ( (v1_relat_1 @ B) & (v1_funct_1 @ B) ) ) ) ) ) , file(funct_1, cc8_funct_1)). thf(cc8_ordinal1, axiom, (! [A: $i] : ( ( (m1_subset_1 @ A) @ k4_ordinal1) => (v7_ordinal1 @ A) ) ) , file(ordinal1, cc8_ordinal1)). thf(cc8_simplex0, axiom, (! [A: $i] : ( (l1_pre_topc @ A) => ( (v4_simplex0 @ A) => ( (v1_matroid0 @ A) & (v2_simplex0 @ A) ) ) ) ) , file(simplex0, cc8_simplex0)). thf(cc8_struct_0, axiom, (! [A: $i] : ( (l1_struct_0 @ A) => ( (v2_struct_0 @ A) => ( (v13_struct_0 @ A) @ k1_xboole_0) ) ) ) , file(struct_0, cc8_struct_0)). thf(cc8_xxreal_0, axiom, (! [A: $i] : ( ( (v1_xxreal_0 @ A) & ( ~ ( (v2_xxreal_0 @ A) ) & ~ ( (v3_xxreal_0 @ A) ) ) ) => ( (v1_xboole_0 @ A) & (v1_xxreal_0 @ A) ) ) ) , file(xxreal_0, cc8_xxreal_0)). thf(cc9_card_1, axiom, (! [A: $i] : ( ( (v3_card_1 @ A) @ 1) => ( ~ ( (v1_xboole_0 @ A) ) & (v1_zfmisc_1 @ A) ) ) ) , file(card_1, cc9_card_1)). thf(cc9_finset_1, axiom, (! [A: $i] : ( ( (v1_xboole_0 @ A) & (v1_relat_1 @ A) ) => ( (v1_relat_1 @ A) & (v2_finset_1 @ A) ) ) ) , file(finset_1, cc9_finset_1)). thf(cc9_funct_1, axiom, (! [A: $i] : ( (v4_funct_1 @ A) => (! [B: $i] : ( ( (m1_subset_1 @ B) @ (k1_zfmisc_1 @ A) ) => (v4_funct_1 @ B) ) ) ) ) , file(funct_1, cc9_funct_1)). thf(cc9_ordinal1, axiom, (! [A: $i] : ( (v1_xboole_0 @ A) => (v6_ordinal1 @ A) ) ) , file(ordinal1, cc9_ordinal1)). thf(cc9_pre_topc, axiom, (! [A: $i] : ( (l1_pre_topc @ A) => ( (v2_struct_0 @ A) => (v6_pre_topc @ A) ) ) ) , file(pre_topc, cc9_pre_topc)). thf(cc9_simplex0, axiom, (! [A: $i] : ( (l1_pre_topc @ A) => ( (v2_simplex0 @ A) => ( (v4_matroid0 @ A) & (v3_simplex0 @ A) ) ) ) ) , file(simplex0, cc9_simplex0)). thf(cc9_struct_0, axiom, (! [A: $i] : ( (l1_struct_0 @ A) => ( ( (v13_struct_0 @ A) @ k1_xboole_0) => (v2_struct_0 @ A) ) ) ) , file(struct_0, cc9_struct_0)). thf(commutativity_k1_xxreal_3, axiom, (! [A: $i, B: $i] : ( ( (v1_xxreal_0 @ A) & (v1_xxreal_0 @ B) ) => ( (= @ ( (k1_xxreal_3 @ A) @ B) ) @ ( (k1_xxreal_3 @ B) @ A) ) ) ) , file(xxreal_3, k1_xxreal_3)). thf(commutativity_k2_xcmplx_0, axiom, (! [A: $i, B: $i] : ( ( (v1_xcmplx_0 @ A) & (v1_xcmplx_0 @ B) ) => ( (= @ ( (k2_xcmplx_0 @ A) @ B) ) @ ( (k2_xcmplx_0 @ B) @ A) ) ) ) , file(xcmplx_0, k2_xcmplx_0)). thf(connectedness_r1_ordinal1, axiom, (! [A: $i, B: $i] : ( ( (v3_ordinal1 @ A) & (v3_ordinal1 @ B) ) => ( ( (r1_ordinal1 @ A) @ B) | ( (r1_ordinal1 @ B) @ A) ) ) ) , file(ordinal1, r1_ordinal1)). thf(connectedness_r1_xxreal_0, axiom, (! [A: $i, B: $i] : ( ( (v1_xxreal_0 @ A) & (v1_xxreal_0 @ B) ) => ( ( (r1_xxreal_0 @ A) @ B) | ( (r1_xxreal_0 @ B) @ A) ) ) ) , file(xxreal_0, r1_xxreal_0)). thf(d11_simplex0, axiom, (! [A: $i] : (! [B: $i] : ( ( (m1_subset_1 @ B) @ (k1_zfmisc_1 @ (k1_zfmisc_1 @ A) ) ) => ( (= @ ( (k5_simplex0 @ A) @ B) ) @ ( (g1_pre_topc @ A) @ ( (k2_simplex0 @ A) @ B) ) ) ) ) ) , file(simplex0, d11_simplex0)). thf(d17_simplex0, axiom, (! [A: $i] : (! [B: $i] : ( ( (m1_simplex0 @ B) @ A) => (! [C: $i] : ( (v1_xreal_0 @ C) => ( (= @ ( ( (k8_simplex0 @ A) @ B) @ C) ) @ ( (k5_simplex0 @ (u1_struct_0 @ B) ) @ ( ( (k3_simplex0 @ (u1_struct_0 @ B) ) @ (u1_pre_topc @ B) ) @ ( (k1_xxreal_3 @ C) @ 1) ) ) ) ) ) ) ) ) , file(simplex0, d17_simplex0)). thf(d1_matroid0, axiom, (! [A: $i] : ( (l1_pre_topc @ A) => ( (= @ (k1_matroid0 @ A) ) @ (u1_pre_topc @ A) ) ) ) , file(matroid0, d1_matroid0)). thf(d2_pre_topc, axiom, (! [A: $i] : ( (l1_pre_topc @ A) => (! [B: $i] : ( ( (m1_subset_1 @ B) @ (k1_zfmisc_1 @ (u1_struct_0 @ A) ) ) => ( ( (v3_pre_topc @ B) @ A) <=> ( (r2_hidden @ B) @ (u1_pre_topc @ A) ) ) ) ) ) ) , file(pre_topc, d2_pre_topc)). thf(d2_simplex0, axiom, (! [A: $i] : (! [B: $i] : (! [C: $i] : (! [D: $i] : ( ( (m1_subset_1 @ D) @ (k1_zfmisc_1 @ (k1_zfmisc_1 @ A) ) ) => ( ( (= @ D) @ ( ( (k3_simplex0 @ A) @ B) @ C) ) <=> (! [E: $i] : ( ( (m1_subset_1 @ E) @ (k1_zfmisc_1 @ A) ) => ( ( (r2_hidden @ E) @ D) <=> ( ( (r2_hidden @ E) @ B) & ( (r1_ordinal1 @ (k1_card_1 @ E) ) @ (k1_card_1 @ C) ) ) ) ) ) ) ) ) ) ) ) , file(simplex0, d2_simplex0)). thf(d2_xboole_0, axiom, ( (= @ k1_xboole_0) @ (eps @ (^ [A: $i] : (v1_xboole_0 @ A) ) ) ) , file(xboole_0, d2_xboole_0)). thf(d6_finset_1, axiom, (! [A: $i] : ( (v5_finset_1 @ A) <=> (! [B: $i] : ( ( (r2_hidden @ B) @ A) => (v1_finset_1 @ B) ) ) ) ) , file(finset_1, d6_finset_1)). thf(d6_matroid0, axiom, (! [A: $i] : ( (l1_pre_topc @ A) => ( (v3_matroid0 @ A) <=> (v5_finset_1 @ (k1_matroid0 @ A) ) ) ) ) , file(matroid0, d6_matroid0)). thf(dt_g1_pre_topc, axiom, (! [A: $i, B: $i] : ( ( (m1_subset_1 @ B) @ (k1_zfmisc_1 @ (k1_zfmisc_1 @ A) ) ) => ( (v1_pre_topc @ ( (g1_pre_topc @ A) @ B) ) & (l1_pre_topc @ ( (g1_pre_topc @ A) @ B) ) ) ) ) , file(pre_topc, g1_pre_topc)). thf(dt_k1_card_1, axiom, (! [A: $i] : (v1_card_1 @ (k1_card_1 @ A) ) ) , file(card_1, k1_card_1)). thf(dt_k1_matroid0, axiom, (! [A: $i] : ( (l1_pre_topc @ A) => ( (m1_subset_1 @ (k1_matroid0 @ A) ) @ (k1_zfmisc_1 @ (k1_zfmisc_1 @ (u1_struct_0 @ A) ) ) ) ) ) , file(matroid0, k1_matroid0)). thf(dt_k1_numbers, axiom, $true, file(numbers, k1_numbers)). thf(dt_k1_simplex0, axiom, (! [A: $i] : (v1_classes1 @ (k1_simplex0 @ A) ) ) , file(simplex0, k1_simplex0)). thf(dt_k1_xboole_0, axiom, $true, file(xboole_0, k1_xboole_0)). thf(dt_k1_xxreal_3, axiom, (! [A: $i, B: $i] : ( ( (v1_xxreal_0 @ A) & (v1_xxreal_0 @ B) ) => (v1_xxreal_0 @ ( (k1_xxreal_3 @ A) @ B) ) ) ) , file(xxreal_3, k1_xxreal_3)). thf(dt_k1_zfmisc_1, axiom, $true, file(zfmisc_1, k1_zfmisc_1)). thf(dt_k2_simplex0, axiom, (! [A: $i, B: $i] : ( ( (m1_subset_1 @ B) @ (k1_zfmisc_1 @ (k1_zfmisc_1 @ A) ) ) => ( (v1_classes1 @ ( (k2_simplex0 @ A) @ B) ) & ( (m1_subset_1 @ ( (k2_simplex0 @ A) @ B) ) @ (k1_zfmisc_1 @ (k1_zfmisc_1 @ A) ) ) ) ) ) , file(simplex0, k2_simplex0)). thf(dt_k2_xcmplx_0, axiom, $true, file(xcmplx_0, k2_xcmplx_0)). thf(dt_k2_xxreal_3, axiom, (! [A: $i] : ( (v1_xxreal_0 @ A) => (v1_xxreal_0 @ (k2_xxreal_3 @ A) ) ) ) , file(xxreal_3, k2_xxreal_3)). thf(dt_k3_simplex0, axiom, (! [A: $i, B: $i, C: $i] : ( (m1_subset_1 @ ( ( (k3_simplex0 @ A) @ B) @ C) ) @ (k1_zfmisc_1 @ (k1_zfmisc_1 @ A) ) ) ) , file(simplex0, k3_simplex0)). thf(dt_k4_ordinal1, axiom, $true, file(ordinal1, k4_ordinal1)). thf(dt_k4_xcmplx_0, axiom, (! [A: $i] : ( (v1_xcmplx_0 @ A) => (v1_xcmplx_0 @ (k4_xcmplx_0 @ A) ) ) ) , file(xcmplx_0, k4_xcmplx_0)). thf(dt_k5_card_1, axiom, (! [A: $i] : ( (v1_finset_1 @ A) => ( (m1_subset_1 @ (k5_card_1 @ A) ) @ k4_ordinal1) ) ) , file(card_1, k5_card_1)). thf(dt_k5_numbers, axiom, ( (m1_subset_1 @ k5_numbers) @ (k1_zfmisc_1 @ k1_numbers) ) , file(numbers, k5_numbers)). thf(dt_k5_simplex0, axiom, (! [A: $i, B: $i] : ( ( (m1_subset_1 @ B) @ (k1_zfmisc_1 @ (k1_zfmisc_1 @ A) ) ) => ( (v1_pre_topc @ ( (k5_simplex0 @ A) @ B) ) & ( (m1_simplex0 @ ( (k5_simplex0 @ A) @ B) ) @ A) ) ) ) , file(simplex0, k5_simplex0)). thf(dt_k6_numbers, axiom, ( ( (m2_subset_1 @ k6_numbers) @ k1_numbers) @ k5_numbers) , file(numbers, k6_numbers)). thf(dt_k6_simplex0, axiom, (! [A: $i] : ( (l1_pre_topc @ A) => (v1_xxreal_0 @ (k6_simplex0 @ A) ) ) ) , file(simplex0, k6_simplex0)). thf(dt_k6_xcmplx_0, axiom, $true, file(xcmplx_0, k6_xcmplx_0)). thf(dt_k7_xcmplx_0, axiom, $true, file(xcmplx_0, k7_xcmplx_0)). thf(dt_k8_simplex0, axiom, (! [A: $i, B: $i, C: $i] : ( ( ( (m1_simplex0 @ B) @ A) & (v1_xreal_0 @ C) ) => ( (m1_simplex0 @ ( ( (k8_simplex0 @ A) @ B) @ C) ) @ A) ) ) , file(simplex0, k8_simplex0)). thf(dt_l1_pre_topc, axiom, (! [A: $i] : ( (l1_pre_topc @ A) => (l1_struct_0 @ A) ) ) , file(pre_topc, l1_pre_topc)). thf(dt_l1_struct_0, axiom, $true, file(struct_0, l1_struct_0)). thf(dt_m1_simplex0, axiom, (! [A: $i] : (! [B: $i] : ( ( (m1_simplex0 @ B) @ A) => (l1_pre_topc @ B) ) ) ) , file(simplex0, m1_simplex0)). thf(dt_m1_subset_1, axiom, $true, file(subset_1, m1_subset_1)). thf(dt_m2_subset_1, axiom, (! [A: $i, B: $i] : ( ( ~ ( (v1_xboole_0 @ A) ) & ( ~ ( (v1_xboole_0 @ B) ) & ( (m1_subset_1 @ B) @ (k1_zfmisc_1 @ A) ) ) ) => (! [C: $i] : ( ( ( (m2_subset_1 @ C) @ A) @ B) => ( (m1_subset_1 @ C) @ A) ) ) ) ) , file(subset_1, m2_subset_1)). thf(dt_u1_pre_topc, axiom, (! [A: $i] : ( (l1_pre_topc @ A) => ( (m1_subset_1 @ (u1_pre_topc @ A) ) @ (k1_zfmisc_1 @ (k1_zfmisc_1 @ (u1_struct_0 @ A) ) ) ) ) ) , file(pre_topc, u1_pre_topc)). thf(dt_u1_struct_0, axiom, $true, file(struct_0, u1_struct_0)). thf(existence_l1_pre_topc, axiom, (? [A: $i] : (l1_pre_topc @ A) ) , file(pre_topc, l1_pre_topc)). thf(existence_l1_struct_0, axiom, (? [A: $i] : (l1_struct_0 @ A) ) , file(struct_0, l1_struct_0)). thf(existence_m1_simplex0, axiom, (! [A: $i] : (? [B: $i] : ( (m1_simplex0 @ B) @ A) ) ) , file(simplex0, m1_simplex0)). thf(existence_m1_subset_1, axiom, (! [A: $i] : (? [B: $i] : ( (m1_subset_1 @ B) @ A) ) ) , file(subset_1, m1_subset_1)). thf(existence_m2_subset_1, axiom, (! [A: $i, B: $i] : ( ( ~ ( (v1_xboole_0 @ A) ) & ( ~ ( (v1_xboole_0 @ B) ) & ( (m1_subset_1 @ B) @ (k1_zfmisc_1 @ A) ) ) ) => (? [C: $i] : ( ( (m2_subset_1 @ C) @ A) @ B) ) ) ) , file(subset_1, m2_subset_1)). thf(fc10_simplex0, axiom, (! [A: $i, B: $i, C: $i] : ( (v1_classes1 @ B) => (v1_classes1 @ ( ( (k3_simplex0 @ A) @ B) @ C) ) ) ) , file(simplex0, fc10_simplex0)). thf(fc10_xreal_0, axiom, (! [A: $i, B: $i] : ( ( ( ~ ( (v2_xxreal_0 @ A) ) & (v1_xreal_0 @ A) ) & ( ~ ( (v2_xxreal_0 @ B) ) & (v1_xreal_0 @ B) ) ) => ~ ( (v2_xxreal_0 @ ( (k2_xcmplx_0 @ A) @ B) ) ) ) ) , file(xreal_0, fc10_xreal_0)). thf(fc10_xxreal_3, axiom, (! [A: $i, B: $i] : ( ( ( (v1_xxreal_0 @ A) & (v2_xxreal_0 @ A) ) & ( (v1_xxreal_0 @ B) & ~ ( (v3_xxreal_0 @ B) ) ) ) => ( (v1_xxreal_0 @ ( (k1_xxreal_3 @ A) @ B) ) & (v2_xxreal_0 @ ( (k1_xxreal_3 @ A) @ B) ) ) ) ) , file(xxreal_3, fc10_xxreal_3)). thf(fc11_simplex0, axiom, (! [A: $i, B: $i, C: $i] : ( ~ ( (v1_setfam_1 @ B) ) => ~ ( (v1_setfam_1 @ ( ( (k3_simplex0 @ A) @ B) @ C) ) ) ) ) , file(simplex0, fc11_simplex0)). thf(fc11_xreal_0, axiom, (! [A: $i, B: $i] : ( ( ( (v2_xxreal_0 @ A) & (v1_xreal_0 @ A) ) & ( ~ ( (v3_xxreal_0 @ B) ) & (v1_xreal_0 @ B) ) ) => (v2_xxreal_0 @ ( (k2_xcmplx_0 @ A) @ B) ) ) ) , file(xreal_0, fc11_xreal_0)). thf(fc11_xxreal_3, axiom, (! [A: $i, B: $i] : ( ( ( (v1_xxreal_0 @ A) & (v2_xxreal_0 @ A) ) & ( (v1_xxreal_0 @ B) & ~ ( (v3_xxreal_0 @ B) ) ) ) => ( (v1_xxreal_0 @ ( (k1_xxreal_3 @ B) @ A) ) & (v2_xxreal_0 @ ( (k1_xxreal_3 @ B) @ A) ) ) ) ) , file(xxreal_3, fc11_xxreal_3)). thf(fc12_simplex0, axiom, (! [A: $i, B: $i, C: $i] : ( ( ~ ( (v1_xboole_0 @ A) ) & ( ( ~ ( (v2_setfam_1 @ B) ) & ( (v1_classes1 @ B) & ( (m1_subset_1 @ B) @ (k1_zfmisc_1 @ (k1_zfmisc_1 @ A) ) ) ) ) & ~ ( (v1_xboole_0 @ C) ) ) ) => ~ ( (v2_setfam_1 @ ( ( (k3_simplex0 @ A) @ B) @ C) ) ) ) ) , file(simplex0, fc12_simplex0)). thf(fc12_xreal_0, axiom, (! [A: $i, B: $i] : ( ( ( (v2_xxreal_0 @ A) & (v1_xreal_0 @ A) ) & ( ~ ( (v3_xxreal_0 @ B) ) & (v1_xreal_0 @ B) ) ) => (v2_xxreal_0 @ ( (k2_xcmplx_0 @ B) @ A) ) ) ) , file(xreal_0, fc12_xreal_0)). thf(fc12_xxreal_3, axiom, (! [A: $i, B: $i] : ( ( ( (v1_xxreal_0 @ A) & (v3_xxreal_0 @ A) ) & ( (v1_xxreal_0 @ B) & ~ ( (v2_xxreal_0 @ B) ) ) ) => ( (v1_xxreal_0 @ ( (k1_xxreal_3 @ A) @ B) ) & (v3_xxreal_0 @ ( (k1_xxreal_3 @ A) @ B) ) ) ) ) , file(xxreal_3, fc12_xxreal_3)). thf(fc13_xreal_0, axiom, (! [A: $i, B: $i] : ( ( ( (v3_xxreal_0 @ A) & (v1_xreal_0 @ A) ) & ( ~ ( (v2_xxreal_0 @ B) ) & (v1_xreal_0 @ B) ) ) => (v3_xxreal_0 @ ( (k2_xcmplx_0 @ A) @ B) ) ) ) , file(xreal_0, fc13_xreal_0)). thf(fc13_xxreal_3, axiom, (! [A: $i, B: $i] : ( ( ( (v1_xxreal_0 @ A) & (v3_xxreal_0 @ A) ) & ( (v1_xxreal_0 @ B) & ~ ( (v2_xxreal_0 @ B) ) ) ) => ( (v1_xxreal_0 @ ( (k1_xxreal_3 @ B) @ A) ) & (v3_xxreal_0 @ ( (k1_xxreal_3 @ B) @ A) ) ) ) ) , file(xxreal_3, fc13_xxreal_3)). thf(fc14_simplex0, axiom, (! [A: $i, B: $i] : ( ( (m1_subset_1 @ B) @ (k1_zfmisc_1 @ (k1_zfmisc_1 @ A) ) ) => ( (v1_pre_topc @ ( (k5_simplex0 @ A) @ B) ) & ( (v1_matroid0 @ ( (k5_simplex0 @ A) @ B) ) & ( (v6_simplex0 @ ( (k5_simplex0 @ A) @ B) ) @ A) ) ) ) ) , file(simplex0, fc14_simplex0)). thf(fc14_xreal_0, axiom, (! [A: $i, B: $i] : ( ( ( (v3_xxreal_0 @ A) & (v1_xreal_0 @ A) ) & ( ~ ( (v2_xxreal_0 @ B) ) & (v1_xreal_0 @ B) ) ) => (v3_xxreal_0 @ ( (k2_xcmplx_0 @ B) @ A) ) ) ) , file(xreal_0, fc14_xreal_0)). thf(fc14_xxreal_3, axiom, (! [A: $i] : ( ( (v1_xxreal_0 @ A) & ~ ( (v2_xxreal_0 @ A) ) ) => ( (v1_xxreal_0 @ (k2_xxreal_3 @ A) ) & ~ ( (v3_xxreal_0 @ (k2_xxreal_3 @ A) ) ) ) ) ) , file(xxreal_3, fc14_xxreal_3)). thf(fc15_simplex0, axiom, (! [A: $i, B: $i] : ( ( ~ ( (v1_xboole_0 @ B) ) & ( (m1_subset_1 @ B) @ (k1_zfmisc_1 @ (k1_zfmisc_1 @ A) ) ) ) => ( (v1_pre_topc @ ( (k5_simplex0 @ A) @ B) ) & ~ ( (v5_simplex0 @ ( (k5_simplex0 @ A) @ B) ) ) ) ) ) , file(simplex0, fc15_simplex0)). thf(fc15_xreal_0, axiom, (! [A: $i] : ( ( ~ ( (v2_xxreal_0 @ A) ) & (v1_xreal_0 @ A) ) => ( (v1_xcmplx_0 @ (k4_xcmplx_0 @ A) ) & ~ ( (v3_xxreal_0 @ (k4_xcmplx_0 @ A) ) ) ) ) ) , file(xreal_0, fc15_xreal_0)). thf(fc15_xxreal_3, axiom, (! [A: $i] : ( ( (v1_xxreal_0 @ A) & ~ ( (v3_xxreal_0 @ A) ) ) => ( (v1_xxreal_0 @ (k2_xxreal_3 @ A) ) & ~ ( (v2_xxreal_0 @ (k2_xxreal_3 @ A) ) ) ) ) ) , file(xxreal_3, fc15_xxreal_3)). thf(fc16_simplex0, axiom, (! [A: $i, B: $i] : ( ( (v5_finset_1 @ B) & ( (m1_subset_1 @ B) @ (k1_zfmisc_1 @ (k1_zfmisc_1 @ A) ) ) ) => ( (v1_pre_topc @ ( (k5_simplex0 @ A) @ B) ) & (v3_matroid0 @ ( (k5_simplex0 @ A) @ B) ) ) ) ) , file(simplex0, fc16_simplex0)). thf(fc16_xreal_0, axiom, (! [A: $i] : ( ( ~ ( (v3_xxreal_0 @ A) ) & (v1_xreal_0 @ A) ) => ( (v1_xcmplx_0 @ (k4_xcmplx_0 @ A) ) & ~ ( (v2_xxreal_0 @ (k4_xcmplx_0 @ A) ) ) ) ) ) , file(xreal_0, fc16_xreal_0)). thf(fc16_xxreal_3, axiom, (! [A: $i] : ( ( (v1_xxreal_0 @ A) & (v2_xxreal_0 @ A) ) => ( (v1_xxreal_0 @ (k2_xxreal_3 @ A) ) & (v3_xxreal_0 @ (k2_xxreal_3 @ A) ) ) ) ) , file(xxreal_3, fc16_xxreal_3)). thf(fc17_finset_1, axiom, (! [A: $i] : ( (v1_finset_1 @ A) => (v1_finset_1 @ (k1_zfmisc_1 @ A) ) ) ) , file(finset_1, fc17_finset_1)). thf(fc17_simplex0, axiom, (! [A: $i, B: $i] : ( ( (v1_finset_1 @ B) & ( (v5_finset_1 @ B) & ( (m1_subset_1 @ B) @ (k1_zfmisc_1 @ (k1_zfmisc_1 @ A) ) ) ) ) => ( (v1_pre_topc @ ( (k5_simplex0 @ A) @ B) ) & (v2_simplex0 @ ( (k5_simplex0 @ A) @ B) ) ) ) ) , file(simplex0, fc17_simplex0)). thf(fc17_xreal_0, axiom, (! [A: $i, B: $i] : ( ( ( ~ ( (v3_xxreal_0 @ A) ) & (v1_xreal_0 @ A) ) & ( ~ ( (v2_xxreal_0 @ B) ) & (v1_xreal_0 @ B) ) ) => ~ ( (v3_xxreal_0 @ ( (k6_xcmplx_0 @ A) @ B) ) ) ) ) , file(xreal_0, fc17_xreal_0)). thf(fc17_xxreal_3, axiom, (! [A: $i] : ( ( (v1_xxreal_0 @ A) & (v3_xxreal_0 @ A) ) => ( (v1_xxreal_0 @ (k2_xxreal_3 @ A) ) & (v2_xxreal_0 @ (k2_xxreal_3 @ A) ) ) ) ) , file(xxreal_3, fc17_xxreal_3)). thf(fc18_simplex0, axiom, (! [A: $i] : ( ( (v4_matroid0 @ A) & (l1_pre_topc @ A) ) => ( (v1_xxreal_0 @ ( (k1_xxreal_3 @ (k6_simplex0 @ A) ) @ 1) ) & (v7_ordinal1 @ ( (k1_xxreal_3 @ (k6_simplex0 @ A) ) @ 1) ) ) ) ) , file(simplex0, fc18_simplex0)). thf(fc18_xreal_0, axiom, (! [A: $i, B: $i] : ( ( ( ~ ( (v3_xxreal_0 @ A) ) & (v1_xreal_0 @ A) ) & ( ~ ( (v2_xxreal_0 @ B) ) & (v1_xreal_0 @ B) ) ) => ~ ( (v2_xxreal_0 @ ( (k6_xcmplx_0 @ B) @ A) ) ) ) ) , file(xreal_0, fc18_xreal_0)). thf(fc19_simplex0, axiom, (! [A: $i] : ( ( (v4_matroid0 @ A) & (l1_pre_topc @ A) ) => ( (v1_xxreal_0 @ (k6_simplex0 @ A) ) & (v1_int_1 @ (k6_simplex0 @ A) ) ) ) ) , file(simplex0, fc19_simplex0)). thf(fc19_struct_0, axiom, (! [A: $i, B: $i] : ( ( (v1_card_1 @ A) & ( ( (v13_struct_0 @ B) @ A) & (l1_struct_0 @ B) ) ) => ( (v3_card_1 @ (u1_struct_0 @ B) ) @ A) ) ) , file(struct_0, fc19_struct_0)). thf(fc19_xreal_0, axiom, (! [A: $i, B: $i] : ( ( ( (v2_xxreal_0 @ A) & (v1_xreal_0 @ A) ) & ( ~ ( (v2_xxreal_0 @ B) ) & (v1_xreal_0 @ B) ) ) => (v2_xxreal_0 @ ( (k6_xcmplx_0 @ A) @ B) ) ) ) , file(xreal_0, fc19_xreal_0)). thf(fc1_card_1, axiom, (! [A: $i] : ( (v1_xboole_0 @ A) => ( (v1_xboole_0 @ (k1_card_1 @ A) ) & (v1_card_1 @ (k1_card_1 @ A) ) ) ) ) , file(card_1, fc1_card_1)). thf(fc1_int_1, axiom, (! [A: $i, B: $i] : ( ( (v1_int_1 @ A) & (v1_int_1 @ B) ) => (v1_int_1 @ ( (k2_xcmplx_0 @ A) @ B) ) ) ) , file(int_1, fc1_int_1)). thf(fc1_matroid0, axiom, (! [A: $i] : ( ( (v1_matroid0 @ A) & (l1_pre_topc @ A) ) => (v1_classes1 @ (k1_matroid0 @ A) ) ) ) , file(matroid0, fc1_matroid0)). thf(fc1_nat_1, axiom, (! [A: $i, B: $i] : ( ( (v7_ordinal1 @ A) & (v7_ordinal1 @ B) ) => (v7_ordinal1 @ ( (k2_xcmplx_0 @ A) @ B) ) ) ) , file(nat_1, fc1_nat_1)). thf(fc1_pencil_1, axiom, (! [A: $i] : ( ( ~ ( (v3_pencil_1 @ A) ) & (l1_pre_topc @ A) ) => ~ ( (v1_xboole_0 @ (u1_pre_topc @ A) ) ) ) ) , file(pencil_1, fc1_pencil_1)). thf(fc1_struct_0, axiom, (! [A: $i] : ( ( (v2_struct_0 @ A) & (l1_struct_0 @ A) ) => (v1_xboole_0 @ (u1_struct_0 @ A) ) ) ) , file(struct_0, fc1_struct_0)). thf(fc1_subset_1, axiom, (! [A: $i] : ~ ( (v1_xboole_0 @ (k1_zfmisc_1 @ A) ) ) ) , file(subset_1, fc1_subset_1)). thf(fc1_xboole_0, axiom, (v1_xboole_0 @ k1_xboole_0) , file(xboole_0, fc1_xboole_0)). thf(fc1_xxreal_3, axiom, (! [A: $i] : ( (v1_xreal_0 @ A) => ( (v1_xxreal_0 @ (k2_xxreal_3 @ A) ) & (v1_xreal_0 @ (k2_xxreal_3 @ A) ) ) ) ) , file(xxreal_3, fc1_xxreal_3)). thf(fc20_simplex0, axiom, (! [A: $i, B: $i] : ( ( (m1_simplex0 @ B) @ A) => (v4_simplex0 @ ( ( (k8_simplex0 @ A) @ B) @ (k2_xxreal_3 @ 1) ) ) ) ) , file(simplex0, fc20_simplex0)). thf(fc20_xreal_0, axiom, (! [A: $i, B: $i] : ( ( ( (v2_xxreal_0 @ A) & (v1_xreal_0 @ A) ) & ( ~ ( (v2_xxreal_0 @ B) ) & (v1_xreal_0 @ B) ) ) => (v3_xxreal_0 @ ( (k6_xcmplx_0 @ B) @ A) ) ) ) , file(xreal_0, fc20_xreal_0)). thf(fc21_simplex0, axiom, (! [A: $i, B: $i, C: $i] : ( ( ( (m1_simplex0 @ B) @ A) & (v1_int_1 @ C) ) => (v4_matroid0 @ ( ( (k8_simplex0 @ A) @ B) @ C) ) ) ) , file(simplex0, fc21_simplex0)). thf(fc21_xreal_0, axiom, (! [A: $i, B: $i] : ( ( ( (v3_xxreal_0 @ A) & (v1_xreal_0 @ A) ) & ( ~ ( (v3_xxreal_0 @ B) ) & (v1_xreal_0 @ B) ) ) => (v3_xxreal_0 @ ( (k6_xcmplx_0 @ A) @ B) ) ) ) , file(xreal_0, fc21_xreal_0)). thf(fc22_simplex0, axiom, (! [A: $i, B: $i, C: $i] : ( ( ( (v4_simplex0 @ B) & ( (m1_simplex0 @ B) @ A) ) & (v1_int_1 @ C) ) => (v4_simplex0 @ ( ( (k8_simplex0 @ A) @ B) @ C) ) ) ) , file(simplex0, fc22_simplex0)). thf(fc22_xreal_0, axiom, (! [A: $i, B: $i] : ( ( ( (v3_xxreal_0 @ A) & (v1_xreal_0 @ A) ) & ( ~ ( (v3_xxreal_0 @ B) ) & (v1_xreal_0 @ B) ) ) => (v2_xxreal_0 @ ( (k6_xcmplx_0 @ B) @ A) ) ) ) , file(xreal_0, fc22_xreal_0)). thf(fc23_simplex0, axiom, (! [A: $i, B: $i, C: $i] : ( ( ~ ( (v1_xboole_0 @ A) ) & ( ( ~ ( (v3_pencil_1 @ B) ) & ( (v1_matroid0 @ B) & ( (m1_simplex0 @ B) @ A) ) ) & (v1_int_1 @ C) ) ) => ~ ( (v3_pencil_1 @ ( ( (k8_simplex0 @ A) @ B) @ C) ) ) ) ) , file(simplex0, fc23_simplex0)). thf(fc2_card_1, axiom, (! [A: $i] : ( ~ ( (v1_xboole_0 @ A) ) => ( ~ ( (v1_xboole_0 @ (k1_card_1 @ A) ) ) & (v1_card_1 @ (k1_card_1 @ A) ) ) ) ) , file(card_1, fc2_card_1)). thf(fc2_cohsp_1, axiom, (! [A: $i] : ( (v1_classes1 @ (k1_zfmisc_1 @ A) ) & (v1_coh_sp @ (k1_zfmisc_1 @ A) ) ) ) , file(cohsp_1, fc2_cohsp_1)). thf(fc2_struct_0, axiom, (! [A: $i] : ( ( ~ ( (v2_struct_0 @ A) ) & (l1_struct_0 @ A) ) => ~ ( (v1_xboole_0 @ (u1_struct_0 @ A) ) ) ) ) , file(struct_0, fc2_struct_0)). thf(fc2_xxreal_3, axiom, (! [A: $i, B: $i] : ( ( (v1_xreal_0 @ A) & (v1_xreal_0 @ B) ) => ( (v1_xxreal_0 @ ( (k1_xxreal_3 @ A) @ B) ) & (v1_xreal_0 @ ( (k1_xxreal_3 @ A) @ B) ) ) ) ) , file(xxreal_3, fc2_xxreal_3)). thf(fc31_finset_1, axiom, (! [A: $i] : ( (v1_finset_1 @ A) => (v5_finset_1 @ (k1_zfmisc_1 @ A) ) ) ) , file(finset_1, fc31_finset_1)). thf(fc31_xreal_0, axiom, (! [A: $i, B: $i] : ( ( ( ~ ( (v3_xxreal_0 @ A) ) & (v1_xreal_0 @ A) ) & ( ~ ( (v2_xxreal_0 @ B) ) & (v1_xreal_0 @ B) ) ) => ~ ( (v2_xxreal_0 @ ( (k7_xcmplx_0 @ A) @ B) ) ) ) ) , file(xreal_0, fc31_xreal_0)). thf(fc32_xreal_0, axiom, (! [A: $i, B: $i] : ( ( ( ~ ( (v3_xxreal_0 @ A) ) & (v1_xreal_0 @ A) ) & ( ~ ( (v2_xxreal_0 @ B) ) & (v1_xreal_0 @ B) ) ) => ~ ( (v2_xxreal_0 @ ( (k7_xcmplx_0 @ B) @ A) ) ) ) ) , file(xreal_0, fc32_xreal_0)). thf(fc33_xreal_0, axiom, (! [A: $i, B: $i] : ( ( ( ~ ( (v3_xxreal_0 @ A) ) & (v1_xreal_0 @ A) ) & ( ~ ( (v3_xxreal_0 @ B) ) & (v1_xreal_0 @ B) ) ) => ~ ( (v3_xxreal_0 @ ( (k7_xcmplx_0 @ A) @ B) ) ) ) ) , file(xreal_0, fc33_xreal_0)). thf(fc34_xreal_0, axiom, (! [A: $i, B: $i] : ( ( ( ~ ( (v2_xxreal_0 @ A) ) & (v1_xreal_0 @ A) ) & ( ~ ( (v2_xxreal_0 @ B) ) & (v1_xreal_0 @ B) ) ) => ~ ( (v3_xxreal_0 @ ( (k7_xcmplx_0 @ A) @ B) ) ) ) ) , file(xreal_0, fc34_xreal_0)). thf(fc3_int_1, axiom, (! [A: $i] : ( (v1_int_1 @ A) => ( (v1_xcmplx_0 @ (k4_xcmplx_0 @ A) ) & (v1_int_1 @ (k4_xcmplx_0 @ A) ) ) ) ) , file(int_1, fc3_int_1)). thf(fc3_nat_1, axiom, (! [A: $i, B: $i] : ( ( (v7_ordinal1 @ A) & ( ~ ( (v1_xboole_0 @ B) ) & (v7_ordinal1 @ B) ) ) => ~ ( (v1_xboole_0 @ ( (k2_xcmplx_0 @ A) @ B) ) ) ) ) , file(nat_1, fc3_nat_1)). thf(fc3_xreal_0, axiom, (! [A: $i] : ( (v1_xreal_0 @ A) => ( (v1_xcmplx_0 @ (k4_xcmplx_0 @ A) ) & (v1_xreal_0 @ (k4_xcmplx_0 @ A) ) ) ) ) , file(xreal_0, fc3_xreal_0)). thf(fc4_card_1, axiom, (v1_card_1 @ k4_ordinal1) , file(card_1, fc4_card_1)). thf(fc4_fib_num2, axiom, (v3_xxreal_2 @ k4_ordinal1) , file(fib_num2, fc4_fib_num2)). thf(fc4_int_1, axiom, (! [A: $i, B: $i] : ( ( (v1_int_1 @ A) & (v1_int_1 @ B) ) => (v1_int_1 @ ( (k6_xcmplx_0 @ A) @ B) ) ) ) , file(int_1, fc4_int_1)). thf(fc4_nat_1, axiom, (! [A: $i, B: $i] : ( ( (v7_ordinal1 @ A) & ( ~ ( (v1_xboole_0 @ B) ) & (v7_ordinal1 @ B) ) ) => ~ ( (v1_xboole_0 @ ( (k2_xcmplx_0 @ B) @ A) ) ) ) ) , file(nat_1, fc4_nat_1)). thf(fc4_xxreal_3, axiom, (! [A: $i, B: $i] : ( ( (v1_xreal_0 @ A) & ( (v1_xxreal_0 @ B) & ~ ( (v1_xreal_0 @ B) ) ) ) => ~ ( (v1_xreal_0 @ ( (k1_xxreal_3 @ A) @ B) ) ) ) ) , file(xxreal_3, fc4_xxreal_3)). thf(fc5_card_1, axiom, (v2_card_1 @ k4_ordinal1) , file(card_1, fc5_card_1)). thf(fc5_simplex0, axiom, ( (v1_xboole_0 @ (k1_simplex0 @ k1_xboole_0) ) & (v1_classes1 @ (k1_simplex0 @ k1_xboole_0) ) ) , file(simplex0, fc5_simplex0)). thf(fc5_xreal_0, axiom, (! [A: $i, B: $i] : ( ( (v1_xreal_0 @ A) & (v1_xreal_0 @ B) ) => (v1_xreal_0 @ ( (k2_xcmplx_0 @ A) @ B) ) ) ) , file(xreal_0, fc5_xreal_0)). thf(fc5_xxreal_3, axiom, (! [A: $i, B: $i] : ( ( ( (v1_xxreal_0 @ A) & ( (v2_xxreal_0 @ A) & ~ ( (v1_xreal_0 @ A) ) ) ) & ( (v1_xxreal_0 @ B) & ( (v2_xxreal_0 @ B) & ~ ( (v1_xreal_0 @ B) ) ) ) ) => ( (v1_xxreal_0 @ ( (k1_xxreal_3 @ A) @ B) ) & ~ ( (v1_xreal_0 @ ( (k1_xxreal_3 @ A) @ B) ) ) ) ) ) , file(xxreal_3, fc5_xxreal_3)). thf(fc6_card_1, axiom, (! [A: $i] : ( (v1_finset_1 @ A) => ( (v1_finset_1 @ (k1_card_1 @ A) ) & (v1_card_1 @ (k1_card_1 @ A) ) ) ) ) , file(card_1, fc6_card_1)). thf(fc6_ordinal1, axiom, ( ~ ( (v1_xboole_0 @ k4_ordinal1) ) & (v3_ordinal1 @ k4_ordinal1) ) , file(ordinal1, fc6_ordinal1)). thf(fc6_simplex0, axiom, (! [A: $i] : ( ~ ( (v1_xboole_0 @ A) ) => ( ~ ( (v1_xboole_0 @ (k1_simplex0 @ A) ) ) & (v1_classes1 @ (k1_simplex0 @ A) ) ) ) ) , file(simplex0, fc6_simplex0)). thf(fc6_struct_0, axiom, (! [A: $i] : ( ( ~ ( (v7_struct_0 @ A) ) & (l1_struct_0 @ A) ) => ~ ( (v1_zfmisc_1 @ (u1_struct_0 @ A) ) ) ) ) , file(struct_0, fc6_struct_0)). thf(fc6_xxreal_3, axiom, (! [A: $i, B: $i] : ( ( ( (v1_xxreal_0 @ A) & ( (v3_xxreal_0 @ A) & ~ ( (v1_xreal_0 @ A) ) ) ) & ( (v1_xxreal_0 @ B) & ( (v3_xxreal_0 @ B) & ~ ( (v1_xreal_0 @ B) ) ) ) ) => ( (v1_xxreal_0 @ ( (k1_xxreal_3 @ A) @ B) ) & ~ ( (v1_xreal_0 @ ( (k1_xxreal_3 @ A) @ B) ) ) ) ) ) , file(xxreal_3, fc6_xxreal_3)). thf(fc7_card_1, axiom, ~ ( (v1_finset_1 @ k4_ordinal1) ) , file(card_1, fc7_card_1)). thf(fc7_pre_topc, axiom, (! [A: $i] : ( ( ~ ( (v2_struct_0 @ A) ) & (l1_pre_topc @ A) ) => ( ~ ( (v2_struct_0 @ ( (g1_pre_topc @ (u1_struct_0 @ A) ) @ (u1_pre_topc @ A) ) ) ) & (v1_pre_topc @ ( (g1_pre_topc @ (u1_struct_0 @ A) ) @ (u1_pre_topc @ A) ) ) ) ) ) , file(pre_topc, fc7_pre_topc)). thf(fc7_simplex0, axiom, (! [A: $i] : ( ~ ( (v2_setfam_1 @ A) ) => ( ~ ( (v2_setfam_1 @ (k1_simplex0 @ A) ) ) & (v1_classes1 @ (k1_simplex0 @ A) ) ) ) ) , file(simplex0, fc7_simplex0)). thf(fc7_struct_0, axiom, (! [A: $i] : ( ( (v7_struct_0 @ A) & (l1_struct_0 @ A) ) => (v1_zfmisc_1 @ (u1_struct_0 @ A) ) ) ) , file(struct_0, fc7_struct_0)). thf(fc7_xreal_0, axiom, (! [A: $i, B: $i] : ( ( (v1_xreal_0 @ A) & (v1_xreal_0 @ B) ) => (v1_xreal_0 @ ( (k6_xcmplx_0 @ A) @ B) ) ) ) , file(xreal_0, fc7_xreal_0)). thf(fc7_xxreal_3, axiom, (! [A: $i, B: $i] : ( ( ( (v1_xxreal_0 @ A) & ( (v3_xxreal_0 @ A) & ~ ( (v1_xreal_0 @ A) ) ) ) & ( (v1_xxreal_0 @ B) & ( (v2_xxreal_0 @ B) & ~ ( (v1_xreal_0 @ B) ) ) ) ) => ( (v1_xboole_0 @ ( (k1_xxreal_3 @ A) @ B) ) & (v1_xxreal_0 @ ( (k1_xxreal_3 @ A) @ B) ) ) ) ) , file(xxreal_3, fc7_xxreal_3)). thf(fc8_card_1, axiom, (! [A: $i] : ( ~ ( (v1_finset_1 @ A) ) => ( ~ ( (v1_finset_1 @ (k1_card_1 @ A) ) ) & (v1_card_1 @ (k1_card_1 @ A) ) ) ) ) , file(card_1, fc8_card_1)). thf(fc8_simplex0, axiom, (! [A: $i] : ( (v5_finset_1 @ A) => ( (v5_finset_1 @ (k1_simplex0 @ A) ) & (v1_classes1 @ (k1_simplex0 @ A) ) ) ) ) , file(simplex0, fc8_simplex0)). thf(fc8_struct_0, axiom, (! [A: $i] : ( ( (v8_struct_0 @ A) & (l1_struct_0 @ A) ) => (v1_finset_1 @ (u1_struct_0 @ A) ) ) ) , file(struct_0, fc8_struct_0)). thf(fc8_xreal_0, axiom, (! [A: $i, B: $i] : ( ( (v1_xreal_0 @ A) & (v1_xreal_0 @ B) ) => (v1_xreal_0 @ ( (k7_xcmplx_0 @ A) @ B) ) ) ) , file(xreal_0, fc8_xreal_0)). thf(fc8_xxreal_3, axiom, (! [A: $i, B: $i] : ( ( ( (v1_xxreal_0 @ A) & ~ ( (v3_xxreal_0 @ A) ) ) & ( (v1_xxreal_0 @ B) & ~ ( (v3_xxreal_0 @ B) ) ) ) => ( (v1_xxreal_0 @ ( (k1_xxreal_3 @ A) @ B) ) & ~ ( (v3_xxreal_0 @ ( (k1_xxreal_3 @ A) @ B) ) ) ) ) ) , file(xxreal_3, fc8_xxreal_3)). thf(fc9_card_1, axiom, (! [A: $i] : ( ~ ( (v1_finset_1 @ A) ) => ~ ( (v1_finset_1 @ (k1_zfmisc_1 @ A) ) ) ) ) , file(card_1, fc9_card_1)). thf(fc9_pre_topc, axiom, (! [A: $i, B: $i] : ( ( ~ ( (v1_xboole_0 @ A) ) & ( (m1_subset_1 @ B) @ (k1_zfmisc_1 @ (k1_zfmisc_1 @ A) ) ) ) => ( ~ ( (v2_struct_0 @ ( (g1_pre_topc @ A) @ B) ) ) & (v1_pre_topc @ ( (g1_pre_topc @ A) @ B) ) ) ) ) , file(pre_topc, fc9_pre_topc)). thf(fc9_simplex0, axiom, (! [A: $i, B: $i, C: $i] : ( (v1_finset_1 @ C) => (v5_finset_1 @ ( ( (k3_simplex0 @ A) @ B) @ C) ) ) ) , file(simplex0, fc9_simplex0)). thf(fc9_struct_0, axiom, (! [A: $i] : ( ( ~ ( (v8_struct_0 @ A) ) & (l1_struct_0 @ A) ) => ~ ( (v1_finset_1 @ (u1_struct_0 @ A) ) ) ) ) , file(struct_0, fc9_struct_0)). thf(fc9_xreal_0, axiom, (! [A: $i, B: $i] : ( ( ( ~ ( (v3_xxreal_0 @ A) ) & (v1_xreal_0 @ A) ) & ( ~ ( (v3_xxreal_0 @ B) ) & (v1_xreal_0 @ B) ) ) => ~ ( (v3_xxreal_0 @ ( (k2_xcmplx_0 @ A) @ B) ) ) ) ) , file(xreal_0, fc9_xreal_0)). thf(fc9_xxreal_3, axiom, (! [A: $i, B: $i] : ( ( ( (v1_xxreal_0 @ A) & ~ ( (v2_xxreal_0 @ A) ) ) & ( (v1_xxreal_0 @ B) & ~ ( (v2_xxreal_0 @ B) ) ) ) => ( (v1_xxreal_0 @ ( (k1_xxreal_3 @ A) @ B) ) & ~ ( (v2_xxreal_0 @ ( (k1_xxreal_3 @ A) @ B) ) ) ) ) ) , file(xxreal_3, fc9_xxreal_3)). thf(free_g1_pre_topc, axiom, (! [A: $i, B: $i] : ( ( (m1_subset_1 @ B) @ (k1_zfmisc_1 @ (k1_zfmisc_1 @ A) ) ) => (! [C: $i, D: $i] : ( ( (= @ ( (g1_pre_topc @ A) @ B) ) @ ( (g1_pre_topc @ C) @ D) ) => ( ( (= @ A) @ C) & ( (= @ B) @ D) ) ) ) ) ) , file(pre_topc, g1_pre_topc)). thf(ie1_xxreal_3, axiom, (! [A: $i, B: $i, C: $i, D: $i] : ( ( (v1_xreal_0 @ A) & ( (v1_xreal_0 @ B) & ( (v1_xcmplx_0 @ C) & (v1_xcmplx_0 @ D) ) ) ) => ( ( ( (= @ A) @ C) & ( (= @ B) @ D) ) => ( (= @ ( (k1_xxreal_3 @ A) @ B) ) @ ( (k2_xcmplx_0 @ C) @ D) ) ) ) ) , file(xxreal_3, ie1_xxreal_3)). thf(ie2_xxreal_3, axiom, (! [A: $i, B: $i] : ( ( (v1_xreal_0 @ A) & (v1_xcmplx_0 @ B) ) => ( ( (= @ A) @ B) => ( (= @ (k2_xxreal_3 @ A) ) @ (k4_xcmplx_0 @ B) ) ) ) ) , file(xxreal_3, ie2_xxreal_3)). thf(involutiveness_k2_xxreal_3, axiom, (! [A: $i] : ( (v1_xxreal_0 @ A) => ( (= @ (k2_xxreal_3 @ (k2_xxreal_3 @ A) ) ) @ A) ) ) , file(xxreal_3, k2_xxreal_3)). thf(involutiveness_k4_xcmplx_0, axiom, (! [A: $i] : ( (v1_xcmplx_0 @ A) => ( (= @ (k4_xcmplx_0 @ (k4_xcmplx_0 @ A) ) ) @ A) ) ) , file(xcmplx_0, k4_xcmplx_0)). thf(projectivity_k1_card_1, axiom, (! [A: $i] : ( (= @ (k1_card_1 @ (k1_card_1 @ A) ) ) @ (k1_card_1 @ A) ) ) , file(card_1, k1_card_1)). thf(projectivity_k5_card_1, axiom, (! [A: $i] : ( (v1_finset_1 @ A) => ( (= @ (k5_card_1 @ (k5_card_1 @ A) ) ) @ (k5_card_1 @ A) ) ) ) , file(card_1, k5_card_1)). thf(rc11_pre_topc, axiom, (? [A: $i] : ( (l1_pre_topc @ A) & ( (v2_struct_0 @ A) & (v1_pre_topc @ A) ) ) ) , file(pre_topc, rc11_pre_topc)). thf(rc1_card_1, axiom, (? [A: $i] : (v1_card_1 @ A) ) , file(card_1, rc1_card_1)). thf(rc1_cohsp_1, axiom, (? [A: $i] : ( ~ ( (v1_xboole_0 @ A) ) & ( (v1_finset_1 @ A) & ( (v1_classes1 @ A) & (v1_coh_sp @ A) ) ) ) ) , file(cohsp_1, rc1_cohsp_1)). thf(rc1_finset_1, axiom, (? [A: $i] : ( ~ ( (v1_xboole_0 @ A) ) & (v1_finset_1 @ A) ) ) , file(finset_1, rc1_finset_1)). thf(rc1_funcop_1, axiom, (? [A: $i] : ( (v1_relat_1 @ A) & ( (v1_funct_1 @ A) & (v1_funcop_1 @ A) ) ) ) , file(funcop_1, rc1_funcop_1)). thf(rc1_funct_1, axiom, (? [A: $i] : ( (v1_relat_1 @ A) & (v1_funct_1 @ A) ) ) , file(funct_1, rc1_funct_1)). thf(rc1_int_1, axiom, (? [A: $i] : ( ( (m1_subset_1 @ A) @ k1_numbers) & ( (v1_xxreal_0 @ A) & ( (v1_xcmplx_0 @ A) & ( (v1_xreal_0 @ A) & (v1_int_1 @ A) ) ) ) ) ) , file(int_1, rc1_int_1)). thf(rc1_nat_1, axiom, (? [A: $i] : ( ~ ( (v1_xboole_0 @ A) ) & ( (v1_ordinal1 @ A) & ( (v2_ordinal1 @ A) & ( (v3_ordinal1 @ A) & ( (v7_ordinal1 @ A) & ( (v1_xcmplx_0 @ A) & ( (v1_xxreal_0 @ A) & ( (v1_xreal_0 @ A) & ( (v1_finset_1 @ A) & (v1_card_1 @ A) ) ) ) ) ) ) ) ) ) ) , file(nat_1, rc1_nat_1)). thf(rc1_ordinal1, axiom, (? [A: $i] : (v3_ordinal1 @ A) ) , file(ordinal1, rc1_ordinal1)). thf(rc1_pre_topc, axiom, (? [A: $i] : ( (l1_pre_topc @ A) & (v1_pre_topc @ A) ) ) , file(pre_topc, rc1_pre_topc)). thf(rc1_relat_1, axiom, (? [A: $i] : ( ~ ( (v1_xboole_0 @ A) ) & (v1_relat_1 @ A) ) ) , file(relat_1, rc1_relat_1)). thf(rc1_setfam_1, axiom, (? [A: $i] : ( ~ ( (v1_xboole_0 @ A) ) & (v1_setfam_1 @ A) ) ) , file(setfam_1, rc1_setfam_1)). thf(rc1_simplex0, axiom, (! [A: $i] : ( ~ ( (v1_xboole_0 @ A) ) => (? [B: $i] : ( ( (m1_subset_1 @ B) @ (k1_zfmisc_1 @ (k1_zfmisc_1 @ A) ) ) & ( ~ ( (v2_setfam_1 @ B) ) & ( (v1_finset_1 @ B) & ( (v5_finset_1 @ B) & (v1_classes1 @ B) ) ) ) ) ) ) ) , file(simplex0, rc1_simplex0)). thf(rc1_subset_1, axiom, (! [A: $i] : ( ~ ( (v1_xboole_0 @ A) ) => (? [B: $i] : ( ( (m1_subset_1 @ B) @ (k1_zfmisc_1 @ A) ) & ~ ( (v1_xboole_0 @ B) ) ) ) ) ) , file(subset_1, rc1_subset_1)). thf(rc1_xboole_0, axiom, (? [A: $i] : (v1_xboole_0 @ A) ) , file(xboole_0, rc1_xboole_0)). thf(rc1_xreal_0, axiom, (? [A: $i] : (v1_xreal_0 @ A) ) , file(xreal_0, rc1_xreal_0)). thf(rc1_xxreal_0, axiom, (? [A: $i] : (v1_xxreal_0 @ A) ) , file(xxreal_0, rc1_xxreal_0)). thf(rc1_xxreal_3, axiom, (? [A: $i] : ( (v1_xxreal_0 @ A) & ( (v2_xxreal_0 @ A) & ~ ( (v1_xreal_0 @ A) ) ) ) ) , file(xxreal_3, rc1_xxreal_3)). thf(rc21_struct_0, axiom, (! [A: $i] : ( ( ~ ( (v2_struct_0 @ A) ) & (l1_struct_0 @ A) ) => (? [B: $i] : ( ( (m1_subset_1 @ B) @ (k1_zfmisc_1 @ (u1_struct_0 @ A) ) ) & ( ~ ( (v1_xboole_0 @ B) ) & (v1_zfmisc_1 @ B) ) ) ) ) ) , file(struct_0, rc21_struct_0)). thf(rc22_struct_0, axiom, (! [A: $i] : ( ( ~ ( (v7_struct_0 @ A) ) & (l1_struct_0 @ A) ) => (? [B: $i] : ( ( (m1_subset_1 @ B) @ (k1_zfmisc_1 @ (u1_struct_0 @ A) ) ) & ~ ( (v1_zfmisc_1 @ B) ) ) ) ) ) , file(struct_0, rc22_struct_0)). thf(rc23_struct_0, axiom, (! [A: $i] : ( (v1_card_1 @ A) => (? [B: $i] : ( (l1_struct_0 @ B) & ( (v13_struct_0 @ B) @ A) ) ) ) ) , file(struct_0, rc23_struct_0)). thf(rc2_card_1, axiom, (? [A: $i] : ( (v1_ordinal1 @ A) & ( (v2_ordinal1 @ A) & ( (v3_ordinal1 @ A) & ( (v1_finset_1 @ A) & (v1_card_1 @ A) ) ) ) ) ) , file(card_1, rc2_card_1)). thf(rc2_cohsp_1, axiom, (! [A: $i] : ( ( ~ ( (v1_xboole_0 @ A) ) & ( (v1_classes1 @ A) & (v1_coh_sp @ A) ) ) => (? [B: $i] : ( ( (m1_subset_1 @ B) @ A) & (v1_finset_1 @ B) ) ) ) ) , file(cohsp_1, rc2_cohsp_1)). thf(rc2_finset_1, axiom, (! [A: $i] : ( ~ ( (v1_xboole_0 @ A) ) => (? [B: $i] : ( ( (m1_subset_1 @ B) @ (k1_zfmisc_1 @ A) ) & ( ~ ( (v1_xboole_0 @ B) ) & (v1_finset_1 @ B) ) ) ) ) ) , file(finset_1, rc2_finset_1)). thf(rc2_funcop_1, axiom, (? [A: $i] : ( (v1_relat_1 @ A) & ( (v1_funct_1 @ A) & ( (v3_funct_1 @ A) & ~ ( (v1_xboole_0 @ A) ) ) ) ) ) , file(funcop_1, rc2_funcop_1)). thf(rc2_funct_1, axiom, (? [A: $i] : ( (v1_relat_1 @ A) & ( (v1_funct_1 @ A) & (v2_funct_1 @ A) ) ) ) , file(funct_1, rc2_funct_1)). thf(rc2_int_1, axiom, (? [A: $i] : (v1_int_1 @ A) ) , file(int_1, rc2_int_1)). thf(rc2_matroid0, axiom, (! [A: $i] : ( ( ~ ( (v3_pencil_1 @ A) ) & (l1_pre_topc @ A) ) => (? [B: $i] : ( ( (m1_subset_1 @ B) @ (k1_zfmisc_1 @ (u1_struct_0 @ A) ) ) & ( (v3_pre_topc @ B) @ A) ) ) ) ) , file(matroid0, rc2_matroid0)). thf(rc2_nat_1, axiom, (? [A: $i] : ( ( (m1_subset_1 @ A) @ (k1_zfmisc_1 @ k1_numbers) ) & ( ~ ( (v1_xboole_0 @ A) ) & (v3_ordinal1 @ A) ) ) ) , file(nat_1, rc2_nat_1)). thf(rc2_ordinal1, axiom, (? [A: $i] : ( ~ ( (v1_xboole_0 @ A) ) & ( (v1_ordinal1 @ A) & ( (v2_ordinal1 @ A) & (v3_ordinal1 @ A) ) ) ) ) , file(ordinal1, rc2_ordinal1)). thf(rc2_relat_1, axiom, (? [A: $i] : ( (v1_relat_1 @ A) & (v2_relat_1 @ A) ) ) , file(relat_1, rc2_relat_1)). thf(rc2_setfam_1, axiom, (? [A: $i] : ~ ( (v2_setfam_1 @ A) ) ) , file(setfam_1, rc2_setfam_1)). thf(rc2_subset_1, axiom, (! [A: $i] : (? [B: $i] : ( ( (m1_subset_1 @ B) @ (k1_zfmisc_1 @ A) ) & (v1_xboole_0 @ B) ) ) ) , file(subset_1, rc2_subset_1)). thf(rc2_xboole_0, axiom, (? [A: $i] : ~ ( (v1_xboole_0 @ A) ) ) , file(xboole_0, rc2_xboole_0)). thf(rc2_xreal_0, axiom, (? [A: $i] : ( (v1_xcmplx_0 @ A) & ( (v1_xxreal_0 @ A) & ( (v2_xxreal_0 @ A) & (v1_xreal_0 @ A) ) ) ) ) , file(xreal_0, rc2_xreal_0)). thf(rc2_xxreal_0, axiom, (? [A: $i] : ( (v1_xxreal_0 @ A) & (v2_xxreal_0 @ A) ) ) , file(xxreal_0, rc2_xxreal_0)). thf(rc2_xxreal_3, axiom, (? [A: $i] : ( (v1_xxreal_0 @ A) & ( (v3_xxreal_0 @ A) & ~ ( (v1_xreal_0 @ A) ) ) ) ) , file(xxreal_3, rc2_xxreal_3)). thf(rc3_card_1, axiom, (? [A: $i] : ~ ( (v1_finset_1 @ A) ) ) , file(card_1, rc3_card_1)). thf(rc3_finset_1, axiom, (? [A: $i] : ( ~ ( (v1_xboole_0 @ A) ) & ( (v1_relat_1 @ A) & ( (v1_funct_1 @ A) & (v1_finset_1 @ A) ) ) ) ) , file(finset_1, rc3_finset_1)). thf(rc3_funct_1, axiom, (? [A: $i] : ( (v1_relat_1 @ A) & ( (v2_relat_1 @ A) & (v1_funct_1 @ A) ) ) ) , file(funct_1, rc3_funct_1)). thf(rc3_matroid0, axiom, (! [A: $i] : ( ( ~ ( (v3_pencil_1 @ A) ) & ( (v1_matroid0 @ A) & (l1_pre_topc @ A) ) ) => (? [B: $i] : ( ( (m1_subset_1 @ B) @ (k1_zfmisc_1 @ (u1_struct_0 @ A) ) ) & ( (v1_finset_1 @ B) & ( (v3_pre_topc @ B) @ A) ) ) ) ) ) , file(matroid0, rc3_matroid0)). thf(rc3_nat_1, axiom, (? [A: $i] : ( ( (m1_subset_1 @ A) @ k5_numbers) & ( ~ ( (v1_xboole_0 @ A) ) & ( (v1_ordinal1 @ A) & ( (v2_ordinal1 @ A) & ( (v3_ordinal1 @ A) & ( (v7_ordinal1 @ A) & ( (v1_xcmplx_0 @ A) & ( (v1_xxreal_0 @ A) & ( (v1_xreal_0 @ A) & ( (v1_finset_1 @ A) & (v1_card_1 @ A) ) ) ) ) ) ) ) ) ) ) ) , file(nat_1, rc3_nat_1)). thf(rc3_setfam_1, axiom, (! [A: $i] : ( ~ ( (v2_setfam_1 @ A) ) => (? [B: $i] : ( ( (m1_subset_1 @ B) @ A) & ~ ( (v1_xboole_0 @ B) ) ) ) ) ) , file(setfam_1, rc3_setfam_1)). thf(rc3_simplex0, axiom, (! [A: $i] : (? [B: $i] : ( ( (m1_simplex0 @ B) @ A) & ( (v2_struct_0 @ B) & ( (v1_pre_topc @ B) & ( (v3_pencil_1 @ B) & (v4_simplex0 @ B) ) ) ) ) ) ) , file(simplex0, rc3_simplex0)). thf(rc3_subset_1, axiom, (! [A: $i] : (? [B: $i] : ( ( (m1_subset_1 @ B) @ (k1_zfmisc_1 @ A) ) & ~ ( ( (v1_subset_1 @ B) @ A) ) ) ) ) , file(subset_1, rc3_subset_1)). thf(rc3_xreal_0, axiom, (? [A: $i] : ( (v1_xcmplx_0 @ A) & ( (v1_xxreal_0 @ A) & ( (v3_xxreal_0 @ A) & (v1_xreal_0 @ A) ) ) ) ) , file(xreal_0, rc3_xreal_0)). thf(rc3_xxreal_0, axiom, (? [A: $i] : ( (v1_xxreal_0 @ A) & (v3_xxreal_0 @ A) ) ) , file(xxreal_0, rc3_xxreal_0)). thf(rc4_card_1, axiom, (! [A: $i] : ( ~ ( (v1_finset_1 @ A) ) => (? [B: $i] : ( ( (m1_subset_1 @ B) @ (k1_zfmisc_1 @ A) ) & ~ ( (v1_finset_1 @ B) ) ) ) ) ) , file(card_1, rc4_card_1)). thf(rc4_funct_1, axiom, (? [A: $i] : ( ~ ( (v1_xboole_0 @ A) ) & ( (v1_relat_1 @ A) & ( (v2_relat_1 @ A) & (v1_funct_1 @ A) ) ) ) ) , file(funct_1, rc4_funct_1)). thf(rc4_ordinal1, axiom, (? [A: $i] : (v7_ordinal1 @ A) ) , file(ordinal1, rc4_ordinal1)). thf(rc4_simplex0, axiom, (! [A: $i] : ( ~ ( (v1_xboole_0 @ A) ) => (? [B: $i] : ( ( (m1_simplex0 @ B) @ A) & ( ~ ( (v2_struct_0 @ B) ) & ( (v1_pre_topc @ B) & ( ~ ( (v3_pencil_1 @ B) ) & ( (v4_simplex0 @ B) & ( (v6_simplex0 @ B) @ A) ) ) ) ) ) ) ) ) , file(simplex0, rc4_simplex0)). thf(rc4_struct_0, axiom, (! [A: $i] : ( ( ~ ( (v2_struct_0 @ A) ) & (l1_struct_0 @ A) ) => (? [B: $i] : ( ( (m1_subset_1 @ B) @ (k1_zfmisc_1 @ (u1_struct_0 @ A) ) ) & ~ ( (v1_xboole_0 @ B) ) ) ) ) ) , file(struct_0, rc4_struct_0)). thf(rc4_subset_1, axiom, (! [A: $i] : ( ~ ( (v1_xboole_0 @ A) ) => (? [B: $i] : ( ( (m1_subset_1 @ B) @ (k1_zfmisc_1 @ A) ) & ( (v1_subset_1 @ B) @ A) ) ) ) ) , file(subset_1, rc4_subset_1)). thf(rc4_xreal_0, axiom, (? [A: $i] : ( (v1_xboole_0 @ A) & ( (v1_xcmplx_0 @ A) & ( (v1_xxreal_0 @ A) & (v1_xreal_0 @ A) ) ) ) ) , file(xreal_0, rc4_xreal_0)). thf(rc4_xxreal_0, axiom, (? [A: $i] : ( (v1_xboole_0 @ A) & (v1_xxreal_0 @ A) ) ) , file(xxreal_0, rc4_xxreal_0)). thf(rc5_card_1, axiom, (! [A: $i] : ( (v1_card_1 @ A) => (? [B: $i] : ( (v3_card_1 @ B) @ A) ) ) ) , file(card_1, rc5_card_1)). thf(rc5_funct_1, axiom, (? [A: $i] : ( (v1_relat_1 @ A) & ( (v1_funct_1 @ A) & ~ ( (v3_funct_1 @ A) ) ) ) ) , file(funct_1, rc5_funct_1)). thf(rc5_ordinal1, axiom, (? [A: $i] : ( ~ ( (v1_xboole_0 @ A) ) & (v7_ordinal1 @ A) ) ) , file(ordinal1, rc5_ordinal1)). thf(rc5_simplex0, axiom, (! [A: $i] : ( ~ ( (v1_xboole_0 @ A) ) => (? [B: $i] : ( ( (m1_simplex0 @ B) @ A) & ( ~ ( (v2_struct_0 @ B) ) & ( (v1_pre_topc @ B) & ( (v1_matroid0 @ B) & ( (v2_simplex0 @ B) & ( ~ ( (v4_simplex0 @ B) ) & ( ~ ( (v5_simplex0 @ B) ) & ( (v6_simplex0 @ B) @ A) ) ) ) ) ) ) ) ) ) ) , file(simplex0, rc5_simplex0)). thf(rc5_subset_1, axiom, (! [A: $i] : ( ~ ( (v1_xboole_0 @ A) ) => (? [B: $i] : ( ( (m1_subset_1 @ B) @ (k1_zfmisc_1 @ A) ) & ( ~ ( (v1_xboole_0 @ B) ) & (v1_zfmisc_1 @ B) ) ) ) ) ) , file(subset_1, rc5_subset_1)). thf(rc6_card_1, axiom, (! [A: $i] : ( (v1_card_1 @ A) => (? [B: $i] : ( (v1_relat_1 @ B) & ( (v1_funct_1 @ B) & ( (v3_card_1 @ B) @ A) ) ) ) ) ) , file(card_1, rc6_card_1)). thf(rc6_cohsp_1, axiom, (? [A: $i] : ( ~ ( (v1_xboole_0 @ A) ) & ( (v2_finsub_1 @ A) & ( (v1_classes1 @ A) & ( (v1_coh_sp @ A) & (v3_cohsp_1 @ A) ) ) ) ) ) , file(cohsp_1, rc6_cohsp_1)). thf(rc6_simplex0, axiom, (? [A: $i] : ( (l1_pre_topc @ A) & ( ~ ( (v2_struct_0 @ A) ) & ( (v1_pre_topc @ A) & ( (v1_matroid0 @ A) & ( (v2_simplex0 @ A) & ( ~ ( (v4_simplex0 @ A) ) & ~ ( (v5_simplex0 @ A) ) ) ) ) ) ) ) ) , file(simplex0, rc6_simplex0)). thf(rc6_subset_1, axiom, (! [A: $i] : ( ~ ( (v1_zfmisc_1 @ A) ) => (? [B: $i] : ( ( (m1_subset_1 @ B) @ (k1_zfmisc_1 @ A) ) & ~ ( (v1_zfmisc_1 @ B) ) ) ) ) ) , file(subset_1, rc6_subset_1)). thf(rc7_card_1, axiom, (! [A: $i] : ( ~ ( (v1_xboole_0 @ A) ) => (? [B: $i] : ( ( (m1_subset_1 @ B) @ (k1_zfmisc_1 @ A) ) & ( (v3_card_1 @ B) @ 1) ) ) ) ) , file(card_1, rc7_card_1)). thf(rc7_finset_1, axiom, (! [A: $i] : ( ~ ( (v1_zfmisc_1 @ A) ) => (? [B: $i] : ( ( (m1_subset_1 @ B) @ (k1_zfmisc_1 @ A) ) & ( ~ ( (v1_zfmisc_1 @ B) ) & (v1_finset_1 @ B) ) ) ) ) ) , file(finset_1, rc7_finset_1)). thf(rc7_funct_1, axiom, (? [A: $i] : ( ~ ( (v1_xboole_0 @ A) ) & (v4_funct_1 @ A) ) ) , file(funct_1, rc7_funct_1)). thf(rc7_simplex0, axiom, (! [A: $i] : ( ( ~ ( (v5_simplex0 @ A) ) & (l1_pre_topc @ A) ) => (? [B: $i] : ( ( (m1_subset_1 @ B) @ (k1_zfmisc_1 @ (u1_struct_0 @ A) ) ) & ( (v1_xboole_0 @ B) & ( (v3_pre_topc @ B) @ A) ) ) ) ) ) , file(simplex0, rc7_simplex0)). thf(rc8_finset_1, axiom, (? [A: $i] : ( ~ ( (v1_xboole_0 @ A) ) & ( (v1_finset_1 @ A) & (v5_finset_1 @ A) ) ) ) , file(finset_1, rc8_finset_1)). thf(rc8_simplex0, axiom, (! [A: $i] : ( ( ~ ( (v3_pencil_1 @ A) ) & ( (v3_matroid0 @ A) & (l1_pre_topc @ A) ) ) => (? [B: $i] : ( ( (m1_subset_1 @ B) @ (k1_zfmisc_1 @ (u1_struct_0 @ A) ) ) & ( (v1_finset_1 @ B) & ( (v3_pre_topc @ B) @ A) ) ) ) ) ) , file(simplex0, rc8_simplex0)). thf(rc9_finset_1, axiom, (? [A: $i] : ( ~ ( (v1_xboole_0 @ A) ) & ( (v1_relat_1 @ A) & ( (v1_funct_1 @ A) & (v2_finset_1 @ A) ) ) ) ) , file(finset_1, rc9_finset_1)). thf(redefinition_k2_simplex0, axiom, (! [A: $i, B: $i] : ( ( (m1_subset_1 @ B) @ (k1_zfmisc_1 @ (k1_zfmisc_1 @ A) ) ) => ( (= @ ( (k2_simplex0 @ A) @ B) ) @ (k1_simplex0 @ B) ) ) ) , file(simplex0, k2_simplex0)). thf(redefinition_k5_card_1, axiom, (! [A: $i] : ( (v1_finset_1 @ A) => ( (= @ (k5_card_1 @ A) ) @ (k1_card_1 @ A) ) ) ) , file(card_1, k5_card_1)). thf(redefinition_k5_numbers, axiom, ( (= @ k5_numbers) @ k4_ordinal1) , file(numbers, k5_numbers)). thf(redefinition_k6_numbers, axiom, ( (= @ k6_numbers) @ k1_xboole_0) , file(numbers, k6_numbers)). thf(redefinition_m2_subset_1, axiom, (! [A: $i, B: $i] : ( ( ~ ( (v1_xboole_0 @ A) ) & ( ~ ( (v1_xboole_0 @ B) ) & ( (m1_subset_1 @ B) @ (k1_zfmisc_1 @ A) ) ) ) => (! [C: $i] : ( ( ( (m2_subset_1 @ C) @ A) @ B) <=> ( (m1_subset_1 @ C) @ B) ) ) ) ) , file(subset_1, m2_subset_1)). thf(redefinition_r1_ordinal1, axiom, (! [A: $i, B: $i] : ( ( (v3_ordinal1 @ A) & (v3_ordinal1 @ B) ) => ( ( (r1_ordinal1 @ A) @ B) <=> ( (r1_tarski @ A) @ B) ) ) ) , file(ordinal1, r1_ordinal1)). thf(reflexivity_r1_ordinal1, axiom, (! [A: $i, B: $i] : ( ( (v3_ordinal1 @ A) & (v3_ordinal1 @ B) ) => ( (r1_ordinal1 @ A) @ A) ) ) , file(ordinal1, r1_ordinal1)). thf(reflexivity_r1_tarski, axiom, (! [A: $i, B: $i] : ( (r1_tarski @ A) @ A) ) , file(tarski, r1_tarski)). thf(reflexivity_r1_xxreal_0, axiom, (! [A: $i, B: $i] : ( ( (v1_xxreal_0 @ A) & (v1_xxreal_0 @ B) ) => ( (r1_xxreal_0 @ A) @ A) ) ) , file(xxreal_0, r1_xxreal_0)). thf(rqLessOrEqual__r1_xxreal_0__r0_r0, axiom, ( (r1_xxreal_0 @ 0) @ 0) , file(arithm, rqLessOrEqual__r1_xxreal_0__r0_r0)). thf(rqLessOrEqual__r1_xxreal_0__r0_r1, axiom, ( (r1_xxreal_0 @ 0) @ 1) , file(arithm, rqLessOrEqual__r1_xxreal_0__r0_r1)). thf(rqLessOrEqual__r1_xxreal_0__r0_r2, axiom, ( (r1_xxreal_0 @ 0) @ 2) , file(arithm, rqLessOrEqual__r1_xxreal_0__r0_r2)). thf(rqLessOrEqual__r1_xxreal_0__r0_rm1, axiom, ~ ( ( (r1_xxreal_0 @ 0) @ (k4_xcmplx_0 @ 1) ) ) , file(arithm, rqLessOrEqual__r1_xxreal_0__r0_rm1)). thf(rqLessOrEqual__r1_xxreal_0__r0_rm2, axiom, ~ ( ( (r1_xxreal_0 @ 0) @ (k4_xcmplx_0 @ 2) ) ) , file(arithm, rqLessOrEqual__r1_xxreal_0__r0_rm2)). thf(rqLessOrEqual__r1_xxreal_0__r0_rn1d2, axiom, ( (r1_xxreal_0 @ 0) @ ( (k7_xcmplx_0 @ 1) @ 2) ) , file(arithm, rqLessOrEqual__r1_xxreal_0__r0_rn1d2)). thf(rqLessOrEqual__r1_xxreal_0__r0_rnm1d2, axiom, ~ ( ( (r1_xxreal_0 @ 0) @ ( (k7_xcmplx_0 @ (k4_xcmplx_0 @ 1) ) @ 2) ) ) , file(arithm, rqLessOrEqual__r1_xxreal_0__r0_rnm1d2)). thf(rqLessOrEqual__r1_xxreal_0__r1_r0, axiom, ~ ( ( (r1_xxreal_0 @ 1) @ 0) ) , file(arithm, rqLessOrEqual__r1_xxreal_0__r1_r0)). thf(rqLessOrEqual__r1_xxreal_0__r1_r1, axiom, ( (r1_xxreal_0 @ 1) @ 1) , file(arithm, rqLessOrEqual__r1_xxreal_0__r1_r1)). thf(rqLessOrEqual__r1_xxreal_0__r1_r2, axiom, ( (r1_xxreal_0 @ 1) @ 2) , file(arithm, rqLessOrEqual__r1_xxreal_0__r1_r2)). thf(rqLessOrEqual__r1_xxreal_0__r1_rm1, axiom, ~ ( ( (r1_xxreal_0 @ 1) @ (k4_xcmplx_0 @ 1) ) ) , file(arithm, rqLessOrEqual__r1_xxreal_0__r1_rm1)). thf(rqLessOrEqual__r1_xxreal_0__r1_rm2, axiom, ~ ( ( (r1_xxreal_0 @ 1) @ (k4_xcmplx_0 @ 2) ) ) , file(arithm, rqLessOrEqual__r1_xxreal_0__r1_rm2)). thf(rqLessOrEqual__r1_xxreal_0__r1_rn1d2, axiom, ~ ( ( (r1_xxreal_0 @ 1) @ ( (k7_xcmplx_0 @ 1) @ 2) ) ) , file(arithm, rqLessOrEqual__r1_xxreal_0__r1_rn1d2)). thf(rqLessOrEqual__r1_xxreal_0__r1_rnm1d2, axiom, ~ ( ( (r1_xxreal_0 @ 1) @ ( (k7_xcmplx_0 @ (k4_xcmplx_0 @ 1) ) @ 2) ) ) , file(arithm, rqLessOrEqual__r1_xxreal_0__r1_rnm1d2)). thf(rqLessOrEqual__r1_xxreal_0__r2_r0, axiom, ~ ( ( (r1_xxreal_0 @ 2) @ 0) ) , file(arithm, rqLessOrEqual__r1_xxreal_0__r2_r0)). thf(rqLessOrEqual__r1_xxreal_0__r2_r1, axiom, ~ ( ( (r1_xxreal_0 @ 2) @ 1) ) , file(arithm, rqLessOrEqual__r1_xxreal_0__r2_r1)). thf(rqLessOrEqual__r1_xxreal_0__r2_r2, axiom, ( (r1_xxreal_0 @ 2) @ 2) , file(arithm, rqLessOrEqual__r1_xxreal_0__r2_r2)). thf(rqLessOrEqual__r1_xxreal_0__r2_rm1, axiom, ~ ( ( (r1_xxreal_0 @ 2) @ (k4_xcmplx_0 @ 1) ) ) , file(arithm, rqLessOrEqual__r1_xxreal_0__r2_rm1)). thf(rqLessOrEqual__r1_xxreal_0__r2_rm2, axiom, ~ ( ( (r1_xxreal_0 @ 2) @ (k4_xcmplx_0 @ 2) ) ) , file(arithm, rqLessOrEqual__r1_xxreal_0__r2_rm2)). thf(rqLessOrEqual__r1_xxreal_0__r2_rn1d2, axiom, ~ ( ( (r1_xxreal_0 @ 2) @ ( (k7_xcmplx_0 @ 1) @ 2) ) ) , file(arithm, rqLessOrEqual__r1_xxreal_0__r2_rn1d2)). thf(rqLessOrEqual__r1_xxreal_0__r2_rnm1d2, axiom, ~ ( ( (r1_xxreal_0 @ 2) @ ( (k7_xcmplx_0 @ (k4_xcmplx_0 @ 1) ) @ 2) ) ) , file(arithm, rqLessOrEqual__r1_xxreal_0__r2_rnm1d2)). thf(rqLessOrEqual__r1_xxreal_0__rm1_r0, axiom, ( (r1_xxreal_0 @ (k4_xcmplx_0 @ 1) ) @ 0) , file(arithm, rqLessOrEqual__r1_xxreal_0__rm1_r0)). thf(rqLessOrEqual__r1_xxreal_0__rm1_r1, axiom, ( (r1_xxreal_0 @ (k4_xcmplx_0 @ 1) ) @ 1) , file(arithm, rqLessOrEqual__r1_xxreal_0__rm1_r1)). thf(rqLessOrEqual__r1_xxreal_0__rm1_r2, axiom, ( (r1_xxreal_0 @ (k4_xcmplx_0 @ 1) ) @ 2) , file(arithm, rqLessOrEqual__r1_xxreal_0__rm1_r2)). thf(rqLessOrEqual__r1_xxreal_0__rm1_rm1, axiom, ( (r1_xxreal_0 @ (k4_xcmplx_0 @ 1) ) @ (k4_xcmplx_0 @ 1) ) , file(arithm, rqLessOrEqual__r1_xxreal_0__rm1_rm1)). thf(rqLessOrEqual__r1_xxreal_0__rm1_rm2, axiom, ~ ( ( (r1_xxreal_0 @ (k4_xcmplx_0 @ 1) ) @ (k4_xcmplx_0 @ 2) ) ) , file(arithm, rqLessOrEqual__r1_xxreal_0__rm1_rm2)). thf(rqLessOrEqual__r1_xxreal_0__rm1_rn1d2, axiom, ( (r1_xxreal_0 @ (k4_xcmplx_0 @ 1) ) @ ( (k7_xcmplx_0 @ 1) @ 2) ) , file(arithm, rqLessOrEqual__r1_xxreal_0__rm1_rn1d2)). thf(rqLessOrEqual__r1_xxreal_0__rm1_rnm1d2, axiom, ( (r1_xxreal_0 @ (k4_xcmplx_0 @ 1) ) @ ( (k7_xcmplx_0 @ (k4_xcmplx_0 @ 1) ) @ 2) ) , file(arithm, rqLessOrEqual__r1_xxreal_0__rm1_rnm1d2)). thf(rqLessOrEqual__r1_xxreal_0__rm2_r0, axiom, ( (r1_xxreal_0 @ (k4_xcmplx_0 @ 2) ) @ 0) , file(arithm, rqLessOrEqual__r1_xxreal_0__rm2_r0)). thf(rqLessOrEqual__r1_xxreal_0__rm2_r1, axiom, ( (r1_xxreal_0 @ (k4_xcmplx_0 @ 2) ) @ 1) , file(arithm, rqLessOrEqual__r1_xxreal_0__rm2_r1)). thf(rqLessOrEqual__r1_xxreal_0__rm2_r2, axiom, ( (r1_xxreal_0 @ (k4_xcmplx_0 @ 2) ) @ 2) , file(arithm, rqLessOrEqual__r1_xxreal_0__rm2_r2)). thf(rqLessOrEqual__r1_xxreal_0__rm2_rm1, axiom, ( (r1_xxreal_0 @ (k4_xcmplx_0 @ 2) ) @ (k4_xcmplx_0 @ 1) ) , file(arithm, rqLessOrEqual__r1_xxreal_0__rm2_rm1)). thf(rqLessOrEqual__r1_xxreal_0__rm2_rm2, axiom, ( (r1_xxreal_0 @ (k4_xcmplx_0 @ 2) ) @ (k4_xcmplx_0 @ 2) ) , file(arithm, rqLessOrEqual__r1_xxreal_0__rm2_rm2)). thf(rqLessOrEqual__r1_xxreal_0__rm2_rn1d2, axiom, ( (r1_xxreal_0 @ (k4_xcmplx_0 @ 2) ) @ ( (k7_xcmplx_0 @ 1) @ 2) ) , file(arithm, rqLessOrEqual__r1_xxreal_0__rm2_rn1d2)). thf(rqLessOrEqual__r1_xxreal_0__rn1d2_r0, axiom, ~ ( ( (r1_xxreal_0 @ ( (k7_xcmplx_0 @ 1) @ 2) ) @ 0) ) , file(arithm, rqLessOrEqual__r1_xxreal_0__rn1d2_r0)). thf(rqLessOrEqual__r1_xxreal_0__rn1d2_r1, axiom, ( (r1_xxreal_0 @ ( (k7_xcmplx_0 @ 1) @ 2) ) @ 1) , file(arithm, rqLessOrEqual__r1_xxreal_0__rn1d2_r1)). thf(rqLessOrEqual__r1_xxreal_0__rn1d2_r2, axiom, ( (r1_xxreal_0 @ ( (k7_xcmplx_0 @ 1) @ 2) ) @ 2) , file(arithm, rqLessOrEqual__r1_xxreal_0__rn1d2_r2)). thf(rqLessOrEqual__r1_xxreal_0__rn1d2_rm1, axiom, ~ ( ( (r1_xxreal_0 @ ( (k7_xcmplx_0 @ 1) @ 2) ) @ (k4_xcmplx_0 @ 1) ) ) , file(arithm, rqLessOrEqual__r1_xxreal_0__rn1d2_rm1)). thf(rqLessOrEqual__r1_xxreal_0__rn1d2_rm2, axiom, ~ ( ( (r1_xxreal_0 @ ( (k7_xcmplx_0 @ 1) @ 2) ) @ (k4_xcmplx_0 @ 2) ) ) , file(arithm, rqLessOrEqual__r1_xxreal_0__rn1d2_rm2)). thf(rqLessOrEqual__r1_xxreal_0__rn1d2_rn1d2, axiom, ( (r1_xxreal_0 @ ( (k7_xcmplx_0 @ 1) @ 2) ) @ ( (k7_xcmplx_0 @ 1) @ 2) ) , file(arithm, rqLessOrEqual__r1_xxreal_0__rn1d2_rn1d2)). thf(rqLessOrEqual__r1_xxreal_0__rn1d2_rnm1d2, axiom, ~ ( ( (r1_xxreal_0 @ ( (k7_xcmplx_0 @ 1) @ 2) ) @ ( (k7_xcmplx_0 @ (k4_xcmplx_0 @ 1) ) @ 2) ) ) , file(arithm, rqLessOrEqual__r1_xxreal_0__rn1d2_rnm1d2)). thf(rqLessOrEqual__r1_xxreal_0__rnm1d2_r0, axiom, ( (r1_xxreal_0 @ ( (k7_xcmplx_0 @ (k4_xcmplx_0 @ 1) ) @ 2) ) @ 0) , file(arithm, rqLessOrEqual__r1_xxreal_0__rnm1d2_r0)). thf(rqLessOrEqual__r1_xxreal_0__rnm1d2_r1, axiom, ( (r1_xxreal_0 @ ( (k7_xcmplx_0 @ (k4_xcmplx_0 @ 1) ) @ 2) ) @ 1) , file(arithm, rqLessOrEqual__r1_xxreal_0__rnm1d2_r1)). thf(rqLessOrEqual__r1_xxreal_0__rnm1d2_r2, axiom, ( (r1_xxreal_0 @ ( (k7_xcmplx_0 @ (k4_xcmplx_0 @ 1) ) @ 2) ) @ 2) , file(arithm, rqLessOrEqual__r1_xxreal_0__rnm1d2_r2)). thf(rqLessOrEqual__r1_xxreal_0__rnm1d2_rm1, axiom, ~ ( ( (r1_xxreal_0 @ ( (k7_xcmplx_0 @ (k4_xcmplx_0 @ 1) ) @ 2) ) @ (k4_xcmplx_0 @ 1) ) ) , file(arithm, rqLessOrEqual__r1_xxreal_0__rnm1d2_rm1)). thf(rqLessOrEqual__r1_xxreal_0__rnm1d2_rn1d2, axiom, ( (r1_xxreal_0 @ ( (k7_xcmplx_0 @ (k4_xcmplx_0 @ 1) ) @ 2) ) @ ( (k7_xcmplx_0 @ 1) @ 2) ) , file(arithm, rqLessOrEqual__r1_xxreal_0__rnm1d2_rn1d2)). thf(rqLessOrEqual__r1_xxreal_0__rnm1d2_rnm1d2, axiom, ( (r1_xxreal_0 @ ( (k7_xcmplx_0 @ (k4_xcmplx_0 @ 1) ) @ 2) ) @ ( (k7_xcmplx_0 @ (k4_xcmplx_0 @ 1) ) @ 2) ) , file(arithm, rqLessOrEqual__r1_xxreal_0__rnm1d2_rnm1d2)). thf(rqRealAdd__k2_xcmplx_0__r0_r0_r0, axiom, ( (= @ ( (k2_xcmplx_0 @ 0) @ 0) ) @ 0) , file(arithm, rqRealAdd__k2_xcmplx_0__r0_r0_r0)). thf(rqRealAdd__k2_xcmplx_0__r0_r1_r1, axiom, ( (= @ ( (k2_xcmplx_0 @ 0) @ 1) ) @ 1) , file(arithm, rqRealAdd__k2_xcmplx_0__r0_r1_r1)). thf(rqRealAdd__k2_xcmplx_0__r0_r2_r2, axiom, ( (= @ ( (k2_xcmplx_0 @ 0) @ 2) ) @ 2) , file(arithm, rqRealAdd__k2_xcmplx_0__r0_r2_r2)). thf(rqRealAdd__k2_xcmplx_0__r0_rm1_rm1, axiom, ( (= @ ( (k2_xcmplx_0 @ 0) @ (k4_xcmplx_0 @ 1) ) ) @ (k4_xcmplx_0 @ 1) ) , file(arithm, rqRealAdd__k2_xcmplx_0__r0_rm1_rm1)). thf(rqRealAdd__k2_xcmplx_0__r0_rm2_rm2, axiom, ( (= @ ( (k2_xcmplx_0 @ 0) @ (k4_xcmplx_0 @ 2) ) ) @ (k4_xcmplx_0 @ 2) ) , file(arithm, rqRealAdd__k2_xcmplx_0__r0_rm2_rm2)). thf(rqRealAdd__k2_xcmplx_0__r0_rn1d2_rn1d2, axiom, ( (= @ ( (k2_xcmplx_0 @ 0) @ ( (k7_xcmplx_0 @ 1) @ 2) ) ) @ ( (k7_xcmplx_0 @ 1) @ 2) ) , file(arithm, rqRealAdd__k2_xcmplx_0__r0_rn1d2_rn1d2)). thf(rqRealAdd__k2_xcmplx_0__r0_rnm1d2_rnm1d2, axiom, ( (= @ ( (k2_xcmplx_0 @ 0) @ ( (k7_xcmplx_0 @ (k4_xcmplx_0 @ 1) ) @ 2) ) ) @ ( (k7_xcmplx_0 @ (k4_xcmplx_0 @ 1) ) @ 2) ) , file(arithm, rqRealAdd__k2_xcmplx_0__r0_rnm1d2_rnm1d2)). thf(rqRealAdd__k2_xcmplx_0__r1_r0_r1, axiom, ( (= @ ( (k2_xcmplx_0 @ 1) @ 0) ) @ 1) , file(arithm, rqRealAdd__k2_xcmplx_0__r1_r0_r1)). thf(rqRealAdd__k2_xcmplx_0__r1_r1_r2, axiom, ( (= @ ( (k2_xcmplx_0 @ 1) @ 1) ) @ 2) , file(arithm, rqRealAdd__k2_xcmplx_0__r1_r1_r2)). thf(rqRealAdd__k2_xcmplx_0__r1_rm1_r0, axiom, ( (= @ ( (k2_xcmplx_0 @ 1) @ (k4_xcmplx_0 @ 1) ) ) @ 0) , file(arithm, rqRealAdd__k2_xcmplx_0__r1_rm1_r0)). thf(rqRealAdd__k2_xcmplx_0__r1_rm2_rm1, axiom, ( (= @ ( (k2_xcmplx_0 @ 1) @ (k4_xcmplx_0 @ 2) ) ) @ (k4_xcmplx_0 @ 1) ) , file(arithm, rqRealAdd__k2_xcmplx_0__r1_rm2_rm1)). thf(rqRealAdd__k2_xcmplx_0__r1_rnm1d2_rn1d2, axiom, ( (= @ ( (k2_xcmplx_0 @ 1) @ ( (k7_xcmplx_0 @ (k4_xcmplx_0 @ 1) ) @ 2) ) ) @ ( (k7_xcmplx_0 @ 1) @ 2) ) , file(arithm, rqRealAdd__k2_xcmplx_0__r1_rnm1d2_rn1d2)). thf(rqRealAdd__k2_xcmplx_0__r2_r0_r2, axiom, ( (= @ ( (k2_xcmplx_0 @ 2) @ 0) ) @ 2) , file(arithm, rqRealAdd__k2_xcmplx_0__r2_r0_r2)). thf(rqRealAdd__k2_xcmplx_0__r2_rm1_r1, axiom, ( (= @ ( (k2_xcmplx_0 @ 2) @ (k4_xcmplx_0 @ 1) ) ) @ 1) , file(arithm, rqRealAdd__k2_xcmplx_0__r2_rm1_r1)). thf(rqRealAdd__k2_xcmplx_0__r2_rm2_r0, axiom, ( (= @ ( (k2_xcmplx_0 @ 2) @ (k4_xcmplx_0 @ 2) ) ) @ 0) , file(arithm, rqRealAdd__k2_xcmplx_0__r2_rm2_r0)). thf(rqRealAdd__k2_xcmplx_0__rm1_r0_rm1, axiom, ( (= @ ( (k2_xcmplx_0 @ (k4_xcmplx_0 @ 1) ) @ 0) ) @ (k4_xcmplx_0 @ 1) ) , file(arithm, rqRealAdd__k2_xcmplx_0__rm1_r0_rm1)). thf(rqRealAdd__k2_xcmplx_0__rm1_r1_r0, axiom, ( (= @ ( (k2_xcmplx_0 @ (k4_xcmplx_0 @ 1) ) @ 1) ) @ 0) , file(arithm, rqRealAdd__k2_xcmplx_0__rm1_r1_r0)). thf(rqRealAdd__k2_xcmplx_0__rm1_r2_r1, axiom, ( (= @ ( (k2_xcmplx_0 @ (k4_xcmplx_0 @ 1) ) @ 2) ) @ 1) , file(arithm, rqRealAdd__k2_xcmplx_0__rm1_r2_r1)). thf(rqRealAdd__k2_xcmplx_0__rm1_rm1_rm2, axiom, ( (= @ ( (k2_xcmplx_0 @ (k4_xcmplx_0 @ 1) ) @ (k4_xcmplx_0 @ 1) ) ) @ (k4_xcmplx_0 @ 2) ) , file(arithm, rqRealAdd__k2_xcmplx_0__rm1_rm1_rm2)). thf(rqRealAdd__k2_xcmplx_0__rm1_rn1d2_rnm1d2, axiom, ( (= @ ( (k2_xcmplx_0 @ (k4_xcmplx_0 @ 1) ) @ ( (k7_xcmplx_0 @ 1) @ 2) ) ) @ ( (k7_xcmplx_0 @ (k4_xcmplx_0 @ 1) ) @ 2) ) , file(arithm, rqRealAdd__k2_xcmplx_0__rm1_rn1d2_rnm1d2)). thf(rqRealAdd__k2_xcmplx_0__rm2_r1_rm1, axiom, ( (= @ ( (k2_xcmplx_0 @ (k4_xcmplx_0 @ 2) ) @ 1) ) @ (k4_xcmplx_0 @ 1) ) , file(arithm, rqRealAdd__k2_xcmplx_0__rm2_r1_rm1)). thf(rqRealAdd__k2_xcmplx_0__rm2_r2_r0, axiom, ( (= @ ( (k2_xcmplx_0 @ (k4_xcmplx_0 @ 2) ) @ 2) ) @ 0) , file(arithm, rqRealAdd__k2_xcmplx_0__rm2_r2_r0)). thf(rqRealAdd__k2_xcmplx_0__rn1d2_r0_rn1d2, axiom, ( (= @ ( (k2_xcmplx_0 @ ( (k7_xcmplx_0 @ 1) @ 2) ) @ 0) ) @ ( (k7_xcmplx_0 @ 1) @ 2) ) , file(arithm, rqRealAdd__k2_xcmplx_0__rn1d2_r0_rn1d2)). thf(rqRealAdd__k2_xcmplx_0__rn1d2_rm1_rnm1d2, axiom, ( (= @ ( (k2_xcmplx_0 @ ( (k7_xcmplx_0 @ 1) @ 2) ) @ (k4_xcmplx_0 @ 1) ) ) @ ( (k7_xcmplx_0 @ (k4_xcmplx_0 @ 1) ) @ 2) ) , file(arithm, rqRealAdd__k2_xcmplx_0__rn1d2_rm1_rnm1d2)). thf(rqRealAdd__k2_xcmplx_0__rn1d2_rn1d2_r1, axiom, ( (= @ ( (k2_xcmplx_0 @ ( (k7_xcmplx_0 @ 1) @ 2) ) @ ( (k7_xcmplx_0 @ 1) @ 2) ) ) @ 1) , file(arithm, rqRealAdd__k2_xcmplx_0__rn1d2_rn1d2_r1)). thf(rqRealAdd__k2_xcmplx_0__rn1d2_rnm1d2_r0, axiom, ( (= @ ( (k2_xcmplx_0 @ ( (k7_xcmplx_0 @ 1) @ 2) ) @ ( (k7_xcmplx_0 @ (k4_xcmplx_0 @ 1) ) @ 2) ) ) @ 0) , file(arithm, rqRealAdd__k2_xcmplx_0__rn1d2_rnm1d2_r0)). thf(rqRealAdd__k2_xcmplx_0__rnm1d2_r1_rn1d2, axiom, ( (= @ ( (k2_xcmplx_0 @ ( (k7_xcmplx_0 @ (k4_xcmplx_0 @ 1) ) @ 2) ) @ 1) ) @ ( (k7_xcmplx_0 @ 1) @ 2) ) , file(arithm, rqRealAdd__k2_xcmplx_0__rnm1d2_r1_rn1d2)). thf(rqRealAdd__k2_xcmplx_0__rnm1d2_rn1d2_r0, axiom, ( (= @ ( (k2_xcmplx_0 @ ( (k7_xcmplx_0 @ (k4_xcmplx_0 @ 1) ) @ 2) ) @ ( (k7_xcmplx_0 @ 1) @ 2) ) ) @ 0) , file(arithm, rqRealAdd__k2_xcmplx_0__rnm1d2_rn1d2_r0)). thf(rqRealAdd__k2_xcmplx_0__rnm1d2_rnm1d2_rm1, axiom, ( (= @ ( (k2_xcmplx_0 @ ( (k7_xcmplx_0 @ (k4_xcmplx_0 @ 1) ) @ 2) ) @ ( (k7_xcmplx_0 @ (k4_xcmplx_0 @ 1) ) @ 2) ) ) @ (k4_xcmplx_0 @ 1) ) , file(arithm, rqRealAdd__k2_xcmplx_0__rnm1d2_rnm1d2_rm1)). thf(rqRealDiff__k6_xcmplx_0__r0_r0_r0, axiom, ( (= @ ( (k6_xcmplx_0 @ 0) @ 0) ) @ 0) , file(arithm, rqRealDiff__k6_xcmplx_0__r0_r0_r0)). thf(rqRealDiff__k6_xcmplx_0__r0_r1_rm1, axiom, ( (= @ ( (k6_xcmplx_0 @ 0) @ 1) ) @ (k4_xcmplx_0 @ 1) ) , file(arithm, rqRealDiff__k6_xcmplx_0__r0_r1_rm1)). thf(rqRealDiff__k6_xcmplx_0__r0_r2_rm2, axiom, ( (= @ ( (k6_xcmplx_0 @ 0) @ 2) ) @ (k4_xcmplx_0 @ 2) ) , file(arithm, rqRealDiff__k6_xcmplx_0__r0_r2_rm2)). thf(rqRealDiff__k6_xcmplx_0__r0_rm1_r1, axiom, ( (= @ ( (k6_xcmplx_0 @ 0) @ (k4_xcmplx_0 @ 1) ) ) @ 1) , file(arithm, rqRealDiff__k6_xcmplx_0__r0_rm1_r1)). thf(rqRealDiff__k6_xcmplx_0__r0_rm2_r2, axiom, ( (= @ ( (k6_xcmplx_0 @ 0) @ (k4_xcmplx_0 @ 2) ) ) @ 2) , file(arithm, rqRealDiff__k6_xcmplx_0__r0_rm2_r2)). thf(rqRealDiff__k6_xcmplx_0__r0_rn1d2_rnm1d2, axiom, ( (= @ ( (k6_xcmplx_0 @ 0) @ ( (k7_xcmplx_0 @ 1) @ 2) ) ) @ ( (k7_xcmplx_0 @ (k4_xcmplx_0 @ 1) ) @ 2) ) , file(arithm, rqRealDiff__k6_xcmplx_0__r0_rn1d2_rnm1d2)). thf(rqRealDiff__k6_xcmplx_0__r0_rnm1d2_rn1d2, axiom, ( (= @ ( (k6_xcmplx_0 @ 0) @ ( (k7_xcmplx_0 @ (k4_xcmplx_0 @ 1) ) @ 2) ) ) @ ( (k7_xcmplx_0 @ 1) @ 2) ) , file(arithm, rqRealDiff__k6_xcmplx_0__r0_rnm1d2_rn1d2)). thf(rqRealDiff__k6_xcmplx_0__r1_r0_r1, axiom, ( (= @ ( (k6_xcmplx_0 @ 1) @ 0) ) @ 1) , file(arithm, rqRealDiff__k6_xcmplx_0__r1_r0_r1)). thf(rqRealDiff__k6_xcmplx_0__r1_r1_r0, axiom, ( (= @ ( (k6_xcmplx_0 @ 1) @ 1) ) @ 0) , file(arithm, rqRealDiff__k6_xcmplx_0__r1_r1_r0)). thf(rqRealDiff__k6_xcmplx_0__r1_r2_rm1, axiom, ( (= @ ( (k6_xcmplx_0 @ 1) @ 2) ) @ (k4_xcmplx_0 @ 1) ) , file(arithm, rqRealDiff__k6_xcmplx_0__r1_r2_rm1)). thf(rqRealDiff__k6_xcmplx_0__r1_rm1_r2, axiom, ( (= @ ( (k6_xcmplx_0 @ 1) @ (k4_xcmplx_0 @ 1) ) ) @ 2) , file(arithm, rqRealDiff__k6_xcmplx_0__r1_rm1_r2)). thf(rqRealDiff__k6_xcmplx_0__r1_rn1d2_rn1d2, axiom, ( (= @ ( (k6_xcmplx_0 @ 1) @ ( (k7_xcmplx_0 @ 1) @ 2) ) ) @ ( (k7_xcmplx_0 @ 1) @ 2) ) , file(arithm, rqRealDiff__k6_xcmplx_0__r1_rn1d2_rn1d2)). thf(rqRealDiff__k6_xcmplx_0__r2_r0_r2, axiom, ( (= @ ( (k6_xcmplx_0 @ 2) @ 0) ) @ 2) , file(arithm, rqRealDiff__k6_xcmplx_0__r2_r0_r2)). thf(rqRealDiff__k6_xcmplx_0__r2_r1_r1, axiom, ( (= @ ( (k6_xcmplx_0 @ 2) @ 1) ) @ 1) , file(arithm, rqRealDiff__k6_xcmplx_0__r2_r1_r1)). thf(rqRealDiff__k6_xcmplx_0__r2_r2_r0, axiom, ( (= @ ( (k6_xcmplx_0 @ 2) @ 2) ) @ 0) , file(arithm, rqRealDiff__k6_xcmplx_0__r2_r2_r0)). thf(rqRealDiff__k6_xcmplx_0__rm1_r0_rm1, axiom, ( (= @ ( (k6_xcmplx_0 @ (k4_xcmplx_0 @ 1) ) @ 0) ) @ (k4_xcmplx_0 @ 1) ) , file(arithm, rqRealDiff__k6_xcmplx_0__rm1_r0_rm1)). thf(rqRealDiff__k6_xcmplx_0__rm1_r1_rm2, axiom, ( (= @ ( (k6_xcmplx_0 @ (k4_xcmplx_0 @ 1) ) @ 1) ) @ (k4_xcmplx_0 @ 2) ) , file(arithm, rqRealDiff__k6_xcmplx_0__rm1_r1_rm2)). thf(rqRealDiff__k6_xcmplx_0__rm1_rm1_r0, axiom, ( (= @ ( (k6_xcmplx_0 @ (k4_xcmplx_0 @ 1) ) @ (k4_xcmplx_0 @ 1) ) ) @ 0) , file(arithm, rqRealDiff__k6_xcmplx_0__rm1_rm1_r0)). thf(rqRealDiff__k6_xcmplx_0__rm1_rm2_r1, axiom, ( (= @ ( (k6_xcmplx_0 @ (k4_xcmplx_0 @ 1) ) @ (k4_xcmplx_0 @ 2) ) ) @ 1) , file(arithm, rqRealDiff__k6_xcmplx_0__rm1_rm2_r1)). thf(rqRealDiff__k6_xcmplx_0__rm1_rnm1d2_rnm1d2, axiom, ( (= @ ( (k6_xcmplx_0 @ (k4_xcmplx_0 @ 1) ) @ ( (k7_xcmplx_0 @ (k4_xcmplx_0 @ 1) ) @ 2) ) ) @ ( (k7_xcmplx_0 @ (k4_xcmplx_0 @ 1) ) @ 2) ) , file(arithm, rqRealDiff__k6_xcmplx_0__rm1_rnm1d2_rnm1d2)). thf(rqRealDiff__k6_xcmplx_0__rm2_r0_rm2, axiom, ( (= @ ( (k6_xcmplx_0 @ (k4_xcmplx_0 @ 2) ) @ 0) ) @ (k4_xcmplx_0 @ 2) ) , file(arithm, rqRealDiff__k6_xcmplx_0__rm2_r0_rm2)). thf(rqRealDiff__k6_xcmplx_0__rm2_rm1_rm1, axiom, ( (= @ ( (k6_xcmplx_0 @ (k4_xcmplx_0 @ 2) ) @ (k4_xcmplx_0 @ 1) ) ) @ (k4_xcmplx_0 @ 1) ) , file(arithm, rqRealDiff__k6_xcmplx_0__rm2_rm1_rm1)). thf(rqRealDiff__k6_xcmplx_0__rm2_rm2_r0, axiom, ( (= @ ( (k6_xcmplx_0 @ (k4_xcmplx_0 @ 2) ) @ (k4_xcmplx_0 @ 2) ) ) @ 0) , file(arithm, rqRealDiff__k6_xcmplx_0__rm2_rm2_r0)). thf(rqRealDiff__k6_xcmplx_0__rn1d2_r0_rn1d2, axiom, ( (= @ ( (k6_xcmplx_0 @ ( (k7_xcmplx_0 @ 1) @ 2) ) @ 0) ) @ ( (k7_xcmplx_0 @ 1) @ 2) ) , file(arithm, rqRealDiff__k6_xcmplx_0__rn1d2_r0_rn1d2)). thf(rqRealDiff__k6_xcmplx_0__rn1d2_r1_rnm1d2, axiom, ( (= @ ( (k6_xcmplx_0 @ ( (k7_xcmplx_0 @ 1) @ 2) ) @ 1) ) @ ( (k7_xcmplx_0 @ (k4_xcmplx_0 @ 1) ) @ 2) ) , file(arithm, rqRealDiff__k6_xcmplx_0__rn1d2_r1_rnm1d2)). thf(rqRealDiff__k6_xcmplx_0__rn1d2_rn1d2_r0, axiom, ( (= @ ( (k6_xcmplx_0 @ ( (k7_xcmplx_0 @ 1) @ 2) ) @ ( (k7_xcmplx_0 @ 1) @ 2) ) ) @ 0) , file(arithm, rqRealDiff__k6_xcmplx_0__rn1d2_rn1d2_r0)). thf(rqRealDiff__k6_xcmplx_0__rn1d2_rnm1d2_r1, axiom, ( (= @ ( (k6_xcmplx_0 @ ( (k7_xcmplx_0 @ 1) @ 2) ) @ ( (k7_xcmplx_0 @ (k4_xcmplx_0 @ 1) ) @ 2) ) ) @ 1) , file(arithm, rqRealDiff__k6_xcmplx_0__rn1d2_rnm1d2_r1)). thf(rqRealDiff__k6_xcmplx_0__rnm1d2_r0_rnm1d2, axiom, ( (= @ ( (k6_xcmplx_0 @ ( (k7_xcmplx_0 @ (k4_xcmplx_0 @ 1) ) @ 2) ) @ 0) ) @ ( (k7_xcmplx_0 @ (k4_xcmplx_0 @ 1) ) @ 2) ) , file(arithm, rqRealDiff__k6_xcmplx_0__rnm1d2_r0_rnm1d2)). thf(rqRealDiff__k6_xcmplx_0__rnm1d2_rm1_rn1d2, axiom, ( (= @ ( (k6_xcmplx_0 @ ( (k7_xcmplx_0 @ (k4_xcmplx_0 @ 1) ) @ 2) ) @ (k4_xcmplx_0 @ 1) ) ) @ ( (k7_xcmplx_0 @ 1) @ 2) ) , file(arithm, rqRealDiff__k6_xcmplx_0__rnm1d2_rm1_rn1d2)). thf(rqRealDiff__k6_xcmplx_0__rnm1d2_rn1d2_rm1, axiom, ( (= @ ( (k6_xcmplx_0 @ ( (k7_xcmplx_0 @ (k4_xcmplx_0 @ 1) ) @ 2) ) @ ( (k7_xcmplx_0 @ 1) @ 2) ) ) @ (k4_xcmplx_0 @ 1) ) , file(arithm, rqRealDiff__k6_xcmplx_0__rnm1d2_rn1d2_rm1)). thf(rqRealDiff__k6_xcmplx_0__rnm1d2_rnm1d2_r0, axiom, ( (= @ ( (k6_xcmplx_0 @ ( (k7_xcmplx_0 @ (k4_xcmplx_0 @ 1) ) @ 2) ) @ ( (k7_xcmplx_0 @ (k4_xcmplx_0 @ 1) ) @ 2) ) ) @ 0) , file(arithm, rqRealDiff__k6_xcmplx_0__rnm1d2_rnm1d2_r0)). thf(rqRealDiv__k7_xcmplx_0__r1_r1_r1, axiom, ( (= @ ( (k7_xcmplx_0 @ 1) @ 1) ) @ 1) , file(arithm, rqRealDiv__k7_xcmplx_0__r1_r1_r1)). thf(rqRealDiv__k7_xcmplx_0__r1_r2_rn1d2, axiom, ( (= @ ( (k7_xcmplx_0 @ 1) @ 2) ) @ ( (k7_xcmplx_0 @ 1) @ 2) ) , file(arithm, rqRealDiv__k7_xcmplx_0__r1_r2_rn1d2)). thf(rqRealDiv__k7_xcmplx_0__r1_rm1_rm1, axiom, ( (= @ ( (k7_xcmplx_0 @ 1) @ (k4_xcmplx_0 @ 1) ) ) @ (k4_xcmplx_0 @ 1) ) , file(arithm, rqRealDiv__k7_xcmplx_0__r1_rm1_rm1)). thf(rqRealDiv__k7_xcmplx_0__r1_rm2_rnm1d2, axiom, ( (= @ ( (k7_xcmplx_0 @ 1) @ (k4_xcmplx_0 @ 2) ) ) @ ( (k7_xcmplx_0 @ (k4_xcmplx_0 @ 1) ) @ 2) ) , file(arithm, rqRealDiv__k7_xcmplx_0__r1_rm2_rnm1d2)). thf(rqRealDiv__k7_xcmplx_0__r1_rn1d2_r2, axiom, ( (= @ ( (k7_xcmplx_0 @ 1) @ ( (k7_xcmplx_0 @ 1) @ 2) ) ) @ 2) , file(arithm, rqRealDiv__k7_xcmplx_0__r1_rn1d2_r2)). thf(rqRealDiv__k7_xcmplx_0__r1_rnm1d2_rm2, axiom, ( (= @ ( (k7_xcmplx_0 @ 1) @ ( (k7_xcmplx_0 @ (k4_xcmplx_0 @ 1) ) @ 2) ) ) @ (k4_xcmplx_0 @ 2) ) , file(arithm, rqRealDiv__k7_xcmplx_0__r1_rnm1d2_rm2)). thf(rqRealDiv__k7_xcmplx_0__r2_r1_r2, axiom, ( (= @ ( (k7_xcmplx_0 @ 2) @ 1) ) @ 2) , file(arithm, rqRealDiv__k7_xcmplx_0__r2_r1_r2)). thf(rqRealDiv__k7_xcmplx_0__r2_r2_r1, axiom, ( (= @ ( (k7_xcmplx_0 @ 2) @ 2) ) @ 1) , file(arithm, rqRealDiv__k7_xcmplx_0__r2_r2_r1)). thf(rqRealDiv__k7_xcmplx_0__rm1_r1_rm1, axiom, ( (= @ ( (k7_xcmplx_0 @ (k4_xcmplx_0 @ 1) ) @ 1) ) @ (k4_xcmplx_0 @ 1) ) , file(arithm, rqRealDiv__k7_xcmplx_0__rm1_r1_rm1)). thf(rqRealDiv__k7_xcmplx_0__rm1_r2_rnm1d2, axiom, ( (= @ ( (k7_xcmplx_0 @ (k4_xcmplx_0 @ 1) ) @ 2) ) @ ( (k7_xcmplx_0 @ (k4_xcmplx_0 @ 1) ) @ 2) ) , file(arithm, rqRealDiv__k7_xcmplx_0__rm1_r2_rnm1d2)). thf(rqRealDiv__k7_xcmplx_0__rm2_r2_rm1, axiom, ( (= @ ( (k7_xcmplx_0 @ (k4_xcmplx_0 @ 2) ) @ 2) ) @ (k4_xcmplx_0 @ 1) ) , file(arithm, rqRealDiv__k7_xcmplx_0__rm2_r2_rm1)). thf(rqRealNeg__k4_xcmplx_0__r0_r0, axiom, ( (= @ (k4_xcmplx_0 @ 0) ) @ 0) , file(arithm, rqRealNeg__k4_xcmplx_0__r0_r0)). thf(rqRealNeg__k4_xcmplx_0__r1_rm1, axiom, ( (= @ (k4_xcmplx_0 @ 1) ) @ (k4_xcmplx_0 @ 1) ) , file(arithm, rqRealNeg__k4_xcmplx_0__r1_rm1)). thf(rqRealNeg__k4_xcmplx_0__r2_rm2, axiom, ( (= @ (k4_xcmplx_0 @ 2) ) @ (k4_xcmplx_0 @ 2) ) , file(arithm, rqRealNeg__k4_xcmplx_0__r2_rm2)). thf(rqRealNeg__k4_xcmplx_0__rm1_r1, axiom, ( (= @ (k4_xcmplx_0 @ (k4_xcmplx_0 @ 1) ) ) @ 1) , file(arithm, rqRealNeg__k4_xcmplx_0__rm1_r1)). thf(rqRealNeg__k4_xcmplx_0__rm2_r2, axiom, ( (= @ (k4_xcmplx_0 @ (k4_xcmplx_0 @ 2) ) ) @ 2) , file(arithm, rqRealNeg__k4_xcmplx_0__rm2_r2)). thf(rqRealNeg__k4_xcmplx_0__rn1d2_rnm1d2, axiom, ( (= @ (k4_xcmplx_0 @ ( (k7_xcmplx_0 @ 1) @ 2) ) ) @ ( (k7_xcmplx_0 @ (k4_xcmplx_0 @ 1) ) @ 2) ) , file(arithm, rqRealNeg__k4_xcmplx_0__rn1d2_rnm1d2)). thf(rqRealNeg__k4_xcmplx_0__rnm1d2_rn1d2, axiom, ( (= @ (k4_xcmplx_0 @ ( (k7_xcmplx_0 @ (k4_xcmplx_0 @ 1) ) @ 2) ) ) @ ( (k7_xcmplx_0 @ 1) @ 2) ) , file(arithm, rqRealNeg__k4_xcmplx_0__rnm1d2_rn1d2)). thf(spc0_boole, axiom, (v1_xboole_0 @ 0) , file(boole, spc0_boole)). thf(spc0_numerals, axiom, ( ( ( (m2_subset_1 @ 0) @ k1_numbers) @ k5_numbers) & ( ( (m1_subset_1 @ 0) @ k5_numbers) & ( (m1_subset_1 @ 0) @ k1_numbers) ) ) , file(numerals, spc0_numerals)). thf(spc1_arithm, axiom, (! [A: $i, B: $i] : ( ( (v1_xcmplx_0 @ A) & (v1_xcmplx_0 @ B) ) => ( (= @ ( (k2_xcmplx_0 @ A) @ (k4_xcmplx_0 @ B) ) ) @ ( (k6_xcmplx_0 @ A) @ B) ) ) ) , file(arithm, spc1_arithm)). thf(spc1_boole, axiom, ~ ( (v1_xboole_0 @ 1) ) , file(boole, spc1_boole)). thf(spc1_numerals, axiom, ( ( (v2_xxreal_0 @ 1) & ( ( (m2_subset_1 @ 1) @ k1_numbers) @ k5_numbers) ) & ( ( (m1_subset_1 @ 1) @ k5_numbers) & ( (m1_subset_1 @ 1) @ k1_numbers) ) ) , file(numerals, spc1_numerals)). thf(spc2_boole, axiom, ~ ( (v1_xboole_0 @ 2) ) , file(boole, spc2_boole)). thf(spc2_numerals, axiom, ( ( (v2_xxreal_0 @ 2) & ( ( (m2_subset_1 @ 2) @ k1_numbers) @ k5_numbers) ) & ( ( (m1_subset_1 @ 2) @ k5_numbers) & ( (m1_subset_1 @ 2) @ k1_numbers) ) ) , file(numerals, spc2_numerals)). thf(spc6_arithm, axiom, (! [A: $i, B: $i, C: $i] : ( ( (v1_xcmplx_0 @ A) & ( (v1_xcmplx_0 @ B) & (v1_xcmplx_0 @ C) ) ) => ( (= @ ( (k2_xcmplx_0 @ ( (k2_xcmplx_0 @ A) @ B) ) @ C) ) @ ( (k2_xcmplx_0 @ A) @ ( (k2_xcmplx_0 @ B) @ C) ) ) ) ) , file(arithm, spc6_arithm)). thf(spc8_arithm, axiom, (! [A: $i, B: $i] : ( ( (v1_xcmplx_0 @ A) & (v1_xcmplx_0 @ B) ) => ( (= @ ( (k2_xcmplx_0 @ (k4_xcmplx_0 @ A) ) @ (k4_xcmplx_0 @ B) ) ) @ (k4_xcmplx_0 @ ( (k2_xcmplx_0 @ A) @ B) ) ) ) ) , file(arithm, spc8_arithm)). thf(spc9_arithm, axiom, (! [A: $i, B: $i] : ( ( (v1_xcmplx_0 @ A) & (v1_xcmplx_0 @ B) ) => ( (= @ ( (k6_xcmplx_0 @ (k4_xcmplx_0 @ A) ) @ (k4_xcmplx_0 @ B) ) ) @ ( (k6_xcmplx_0 @ B) @ A) ) ) ) , file(arithm, spc9_arithm)). thf(t11_card_1, axiom, (! [A: $i] : (! [B: $i] : ( ( (r1_tarski @ A) @ B) => ( (r1_ordinal1 @ (k1_card_1 @ A) ) @ (k1_card_1 @ B) ) ) ) ) , file(card_1, t11_card_1)). thf(t1_arithm, axiom, (! [A: $i] : ( (v1_xcmplx_0 @ A) => ( (= @ ( (k2_xcmplx_0 @ A) @ k6_numbers) ) @ A) ) ) , file(arithm, t1_arithm)). thf(t1_numerals, axiom, ( (m1_subset_1 @ k1_xboole_0) @ k4_ordinal1) , file(numerals, t1_numerals)). thf(t1_real, axiom, (! [A: $i] : ( (v1_xreal_0 @ A) => (! [B: $i] : ( (v1_xreal_0 @ B) => ( ( ( (r1_xxreal_0 @ A) @ B) & (v2_xxreal_0 @ A) ) => (v2_xxreal_0 @ B) ) ) ) ) ) , file(real, t1_real)). thf(t1_subset, axiom, (! [A: $i] : (! [B: $i] : ( ( (r2_hidden @ A) @ B) => ( (m1_subset_1 @ A) @ B) ) ) ) , file(subset, t1_subset)). thf(t1_xboole_1, axiom, (! [A: $i] : (! [B: $i] : (! [C: $i] : ( ( ( (r1_tarski @ A) @ B) & ( (r1_tarski @ B) @ C) ) => ( (r1_tarski @ A) @ C) ) ) ) ) , file(xboole_1, t1_xboole_1)). thf(t22_simplex0, axiom, (! [A: $i] : ( (l1_pre_topc @ A) => ( ( (= @ (k6_simplex0 @ A) ) @ (k2_xxreal_3 @ 1) ) <=> (v4_simplex0 @ A) ) ) ) , file(simplex0, t22_simplex0)). thf(t25_simplex0, axiom, (! [A: $i] : ( (v1_int_1 @ A) => (! [B: $i] : ( (l1_pre_topc @ B) => ( ~ ( ( (v3_pencil_1 @ B) & ~ ( ( (r1_xxreal_0 @ (k2_xxreal_3 @ 1) ) @ A) ) ) ) => ( ( (r1_xxreal_0 @ (k6_simplex0 @ B) ) @ A) <=> ( (v3_matroid0 @ B) & (! [C: $i] : ( ( (v1_finset_1 @ C) & ( (m1_subset_1 @ C) @ (k1_zfmisc_1 @ (u1_struct_0 @ B) ) ) ) => ( ( (v3_pre_topc @ C) @ B) => ( (r1_xxreal_0 @ (k5_card_1 @ C) ) @ ( (k1_xxreal_3 @ A) @ 1) ) ) ) ) ) ) ) ) ) ) ) , file(simplex0, t25_simplex0)). thf(t2_real, axiom, (! [A: $i] : ( (v1_xreal_0 @ A) => (! [B: $i] : ( (v1_xreal_0 @ B) => ( ( ( (r1_xxreal_0 @ A) @ B) & (v3_xxreal_0 @ B) ) => (v3_xxreal_0 @ A) ) ) ) ) ) , file(real, t2_real)). thf(t2_simplex0, axiom, (! [A: $i] : (! [B: $i] : ( ( (r2_hidden @ A) @ (k1_simplex0 @ B) ) <=> (? [C: $i] : ( ( (r1_tarski @ A) @ C) & ( (r2_hidden @ C) @ B) ) ) ) ) ) , file(simplex0, t2_simplex0)). thf(t2_subset, axiom, (! [A: $i] : (! [B: $i] : ( ( (m1_subset_1 @ A) @ B) => ( (v1_xboole_0 @ B) | ( (r2_hidden @ A) @ B) ) ) ) ) , file(subset, t2_subset)). thf(t3_int_1, axiom, (! [A: $i] : ( (v1_int_1 @ A) => ( ( (r1_xxreal_0 @ k6_numbers) @ A) => ( (r2_hidden @ A) @ k5_numbers) ) ) ) , file(int_1, t3_int_1)). thf(t3_real, axiom, (! [A: $i] : ( (v1_xreal_0 @ A) => (! [B: $i] : ( (v1_xreal_0 @ B) => ~ ( ( ( (r1_xxreal_0 @ A) @ B) & ( ~ ( (v3_xxreal_0 @ A) ) & (v3_xxreal_0 @ B) ) ) ) ) ) ) ) , file(real, t3_real)). thf(t3_subset, axiom, (! [A: $i] : (! [B: $i] : ( ( (m1_subset_1 @ A) @ (k1_zfmisc_1 @ B) ) <=> ( (r1_tarski @ A) @ B) ) ) ) , file(subset, t3_subset)). thf(t40_nat_1, axiom, (! [A: $i] : ( (v7_ordinal1 @ A) => (! [B: $i] : ( (v7_ordinal1 @ B) => ( ( (r1_ordinal1 @ (k5_card_1 @ A) ) @ (k5_card_1 @ B) ) <=> ( (r1_xxreal_0 @ A) @ B) ) ) ) ) ) , file(nat_1, t40_nat_1)). thf(t4_arithm, axiom, (! [A: $i] : ( (v1_xcmplx_0 @ A) => ( (= @ ( (k6_xcmplx_0 @ A) @ k6_numbers) ) @ A) ) ) , file(arithm, t4_arithm)). thf(t4_real, axiom, (! [A: $i] : ( (v1_xreal_0 @ A) => (! [B: $i] : ( (v1_xreal_0 @ B) => ~ ( ( ( (r1_xxreal_0 @ A) @ B) & ( ~ ( (v2_xxreal_0 @ B) ) & (v2_xxreal_0 @ A) ) ) ) ) ) ) ) , file(real, t4_real)). thf(t4_subset, axiom, (! [A: $i] : (! [B: $i] : (! [C: $i] : ( ( ( (r2_hidden @ A) @ B) & ( (m1_subset_1 @ B) @ (k1_zfmisc_1 @ C) ) ) => ( (m1_subset_1 @ A) @ C) ) ) ) ) , file(subset, t4_subset)). thf(t5_arithm, axiom, (! [A: $i] : ( (v1_xcmplx_0 @ A) => ( (= @ ( (k7_xcmplx_0 @ k6_numbers) @ A) ) @ k6_numbers) ) ) , file(arithm, t5_arithm)). thf(t5_real, axiom, (! [A: $i] : ( (v1_xreal_0 @ A) => (! [B: $i] : ( (v1_xreal_0 @ B) => ( ( (r1_xxreal_0 @ A) @ B) => ( (v1_xboole_0 @ B) | ( (v3_xxreal_0 @ A) | (v2_xxreal_0 @ B) ) ) ) ) ) ) ) , file(real, t5_real)). thf(t5_subset, axiom, (! [A: $i] : (! [B: $i] : (! [C: $i] : ~ ( ( ( (r2_hidden @ A) @ B) & ( ( (m1_subset_1 @ B) @ (k1_zfmisc_1 @ C) ) & (v1_xboole_0 @ C) ) ) ) ) ) ) , file(subset, t5_subset)). thf(t6_arithm, axiom, (! [A: $i] : ( (v1_xcmplx_0 @ A) => ( (= @ ( (k7_xcmplx_0 @ A) @ 1) ) @ A) ) ) , file(arithm, t6_arithm)). thf(t6_boole, axiom, (! [A: $i] : ( (v1_xboole_0 @ A) => ( (= @ A) @ k1_xboole_0) ) ) , file(boole, t6_boole)). thf(t6_real, axiom, (! [A: $i] : ( (v1_xreal_0 @ A) => (! [B: $i] : ( (v1_xreal_0 @ B) => ( ( (r1_xxreal_0 @ A) @ B) => ( (v1_xboole_0 @ A) | ( (v2_xxreal_0 @ B) | (v3_xxreal_0 @ A) ) ) ) ) ) ) ) , file(real, t6_real)). thf(t6_xreal_1, axiom, (! [A: $i] : ( (v1_xreal_0 @ A) => (! [B: $i] : ( (v1_xreal_0 @ B) => (! [C: $i] : ( (v1_xreal_0 @ C) => ( ( (r1_xxreal_0 @ A) @ B) <=> ( (r1_xxreal_0 @ ( (k2_xcmplx_0 @ A) @ C) ) @ ( (k2_xcmplx_0 @ B) @ C) ) ) ) ) ) ) ) ) , file(xreal_1, t6_xreal_1)). thf(t7_boole, axiom, (! [A: $i] : (! [B: $i] : ~ ( ( ( (r2_hidden @ A) @ B) & (v1_xboole_0 @ B) ) ) ) ) , file(boole, t7_boole)). thf(t7_real, axiom, (! [A: $i] : ( (v1_xreal_0 @ A) => (! [B: $i] : ( (v1_xreal_0 @ B) => ~ ( ( ~ ( ( (r1_xxreal_0 @ A) @ B) ) & ( ~ ( (v2_xxreal_0 @ A) ) & ~ ( (v3_xxreal_0 @ B) ) ) ) ) ) ) ) ) , file(real, t7_real)). thf(t8_boole, axiom, (! [A: $i] : (! [B: $i] : ~ ( ( (v1_xboole_0 @ A) & ( ~ ( ( (= @ A) @ B) ) & (v1_xboole_0 @ B) ) ) ) ) ) , file(boole, t8_boole)). thf(t8_real, axiom, (! [A: $i] : ( (v1_xreal_0 @ A) => (! [B: $i] : ( (v1_xreal_0 @ B) => ~ ( ( ~ ( ( (r1_xxreal_0 @ A) @ B) ) & ( ~ ( (v3_xxreal_0 @ B) ) & ~ ( (v2_xxreal_0 @ A) ) ) ) ) ) ) ) ) , file(real, t8_real)). thf(t45_simplex0, conjecture, (! [A: $i] : (! [B: $i] : ( (v1_int_1 @ B) => (! [C: $i] : ( ( (m1_simplex0 @ C) @ A) => ( ( ( (r1_xxreal_0 @ (k2_xxreal_3 @ 1) ) @ B) & ( (= @ ( ( (k8_simplex0 @ A) @ C) @ B) ) @ ( (g1_pre_topc @ (u1_struct_0 @ C) ) @ (u1_pre_topc @ C) ) ) ) => ( (r1_xxreal_0 @ (k6_simplex0 @ C) ) @ B) ) ) ) ) ) ) , file(simplex0, t45_simplex0)).