include('Axioms/SET010^0.ax').
thf(m2_funct_2_type, type, m2_funct_2: $i > $i > $i > $i > $o).
thf(k8_funcop_1_type, type, k8_funcop_1: $i > $i > $i > $i).
thf(u1_struct_0_type, type, u1_struct_0: $i > $i).
thf(k2_bspace_type, type, k2_bspace: $i).
thf(k2_zfmisc_1_type, type, k2_zfmisc_1: $i > $i > $i).
thf(k5_struct_0_type, type, k5_struct_0: $i > $i).
thf(k2_tarski_type, type, k2_tarski: $i > $i > $i).
thf(k4_struct_0_type, type, k4_struct_0: $i > $i).
thf(k9_funct_2_type, type, k9_funct_2: $i > $i > $i).
thf(r1_tarski_type, type, r1_tarski: $i > $i > $o).
thf(k1_tarski_type, type, k1_tarski: $i > $i).
thf(m1_subset_1_type, type, m1_subset_1: $i > $i > $o).
thf(k9_xtuple_0_type, type, k9_xtuple_0: $i > $i).
thf(k2_funcop_1_type, type, k2_funcop_1: $i > $i > $i).
thf(k10_xtuple_0_type, type, k10_xtuple_0: $i > $i).
thf(v1_xboole_0_type, type, v1_xboole_0: $i > $o).
thf(m1_funct_2_type, type, m1_funct_2: $i > $i > $i > $o).
thf(k1_funct_2_type, type, k1_funct_2: $i > $i > $i).
thf(v2_struct_0_type, type, v2_struct_0: $i > $o).
thf(l1_struct_0_type, type, l1_struct_0: $i > $o).
thf(v1_relat_1_type, type, v1_relat_1: $i > $o).
thf(v1_funct_1_type, type, v1_funct_1: $i > $o).
thf(l6_algstr_0_type, type, l6_algstr_0: $i > $o).
thf(l2_algstr_0_type, type, l2_algstr_0: $i > $o).
thf(l5_algstr_0_type, type, l5_algstr_0: $i > $o).
thf(l4_algstr_0_type, type, l4_algstr_0: $i > $o).
thf(l4_struct_0_type, type, l4_struct_0: $i > $o).
thf(l3_struct_0_type, type, l3_struct_0: $i > $o).
thf(l3_algstr_0_type, type, l3_algstr_0: $i > $o).
thf(l2_struct_0_type, type, l2_struct_0: $i > $o).
thf(l1_algstr_0_type, type, l1_algstr_0: $i > $o).
thf(v6_struct_0_type, type, v6_struct_0: $i > $o).
thf(v13_algstr_0_type, type, v13_algstr_0: $i > $o).
thf(v33_algstr_0_type, type, v33_algstr_0: $i > $o).
thf(v3_group_1_type, type, v3_group_1: $i > $o).
thf(v5_group_1_type, type, v5_group_1: $i > $o).
thf(v4_vectsp_1_type, type, v4_vectsp_1: $i > $o).
thf(v5_vectsp_1_type, type, v5_vectsp_1: $i > $o).
thf(v2_rlvect_1_type, type, v2_rlvect_1: $i > $o).
thf(v3_rlvect_1_type, type, v3_rlvect_1: $i > $o).
thf(v4_rlvect_1_type, type, v4_rlvect_1: $i > $o).
thf(t7_zfmisc_1, axiom,   (! [A: $i] :  (! [B: $i] :  ( (r1_tarski @  (k1_tarski @ A) )  @  ( (k2_tarski @ A)  @ B) ) ) ) , file(zfmisc_1, t7_zfmisc_1)).
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(t1_subset, axiom,   (! [A: $i] :  (! [B: $i] :  ( ( (r2_hidden @ A)  @ B)  =>  ( (m1_subset_1 @ A)  @ B) ) ) ) , file(subset, t1_subset)).
thf(t13_funcop_1, axiom,   (! [A: $i] :  (! [B: $i] :  ( ( (= @  (k9_xtuple_0 @  ( (k2_funcop_1 @ A)  @ B) ) )  @ A)  &  ( (r1_tarski @  (k10_xtuple_0 @  ( (k2_funcop_1 @ A)  @ B) ) )  @  (k1_tarski @ B) ) ) ) ) , file(funcop_1, t13_funcop_1)).
thf(redefinition_m2_funct_2, axiom,   (! [A: $i, B: $i, C: $i] :  ( ( ~ ( (v1_xboole_0 @ B) )  &  ( ( (m1_funct_2 @ C)  @ A)  @ B) )  =>  (! [D: $i] :  ( ( ( ( (m2_funct_2 @ D)  @ A)  @ B)  @ C)  <=>  ( (m1_subset_1 @ D)  @ C) ) ) ) ) , file(funct_2, m2_funct_2)).
thf(redefinition_k9_funct_2, axiom,   (! [A: $i, B: $i] :  ( ~ ( (v1_xboole_0 @ B) )  =>  ( (= @  ( (k9_funct_2 @ A)  @ B) )  @  ( (k1_funct_2 @ A)  @ B) ) ) ) , file(funct_2, k9_funct_2)).
thf(redefinition_k8_funcop_1, axiom,   (! [A: $i, B: $i, C: $i] :  ( ( ~ ( (v1_xboole_0 @ A) )  &  ( (m1_subset_1 @ C)  @ A) )  =>  ( (= @  ( ( (k8_funcop_1 @ A)  @ B)  @ C) )  @  ( (k2_funcop_1 @ B)  @ C) ) ) ) , file(funcop_1, k8_funcop_1)).
thf(fc3_xboole_0, axiom,   (! [A: $i, B: $i] :  ~ ( (v1_xboole_0 @  ( (k2_tarski @ A)  @ B) ) ) ) , file(xboole_0, fc3_xboole_0)).
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(fc1_funcop_1, axiom,   (! [A: $i, B: $i] :  ( (v1_relat_1 @  ( (k2_funcop_1 @ A)  @ B) )  &  (v1_funct_1 @  ( (k2_funcop_1 @ A)  @ B) ) ) ) , file(funcop_1, fc1_funcop_1)).
thf(dt_l6_algstr_0, axiom,   (! [A: $i] :  ( (l6_algstr_0 @ A)  =>  ( (l2_algstr_0 @ A)  &  (l5_algstr_0 @ A) ) ) ) , file(algstr_0, l6_algstr_0)).
thf(dt_l5_algstr_0, axiom,   (! [A: $i] :  ( (l5_algstr_0 @ A)  =>  ( (l4_algstr_0 @ A)  &  (l4_struct_0 @ A) ) ) ) , file(algstr_0, l5_algstr_0)).
thf(dt_l4_algstr_0, axiom,   (! [A: $i] :  ( (l4_algstr_0 @ A)  =>  ( (l3_struct_0 @ A)  &  (l3_algstr_0 @ A) ) ) ) , file(algstr_0, l4_algstr_0)).
thf(dt_l2_struct_0, axiom,   (! [A: $i] :  ( (l2_struct_0 @ A)  =>  (l1_struct_0 @ A) ) ) , file(struct_0, l2_struct_0)).
thf(dt_l2_algstr_0, axiom,   (! [A: $i] :  ( (l2_algstr_0 @ A)  =>  ( (l2_struct_0 @ A)  &  (l1_algstr_0 @ A) ) ) ) , file(algstr_0, l2_algstr_0)).
thf(dt_k9_funct_2, axiom,   (! [A: $i, B: $i] :  ( ~ ( (v1_xboole_0 @ B) )  =>  ( ( (m1_funct_2 @  ( (k9_funct_2 @ A)  @ B) )  @ A)  @ B) ) ) , file(funct_2, k9_funct_2)).
thf(dt_k5_struct_0, axiom,   (! [A: $i] :  ( (l3_struct_0 @ A)  =>  ( (m1_subset_1 @  (k5_struct_0 @ A) )  @  (u1_struct_0 @ A) ) ) ) , file(struct_0, k5_struct_0)).
thf(dt_k2_bspace, axiom,   ( ~ ( (v2_struct_0 @ k2_bspace) )  &  ( ~ ( (v6_struct_0 @ k2_bspace) )  &  ( (v13_algstr_0 @ k2_bspace)  &  ( (v33_algstr_0 @ k2_bspace)  &  ( (v3_group_1 @ k2_bspace)  &  ( (v5_group_1 @ k2_bspace)  &  ( (v4_vectsp_1 @ k2_bspace)  &  ( (v5_vectsp_1 @ k2_bspace)  &  ( (v2_rlvect_1 @ k2_bspace)  &  ( (v3_rlvect_1 @ k2_bspace)  &  ( (v4_rlvect_1 @ k2_bspace)  &  (l6_algstr_0 @ k2_bspace) ) ) ) ) ) ) ) ) ) ) ) , file(bspace, k2_bspace)).
thf(d2_funct_2, axiom,   (! [A: $i] :  (! [B: $i] :  (! [C: $i] :  ( ( (= @ C)  @  ( (k1_funct_2 @ A)  @ B) )  <=>  (! [D: $i] :  ( ( (r2_hidden @ D)  @ C)  <=>  (? [E: $i] :  ( ( (v1_relat_1 @ E)  &  (v1_funct_1 @ E) )  &  ( ( (= @ D)  @ E)  &  ( ( (= @  (k9_xtuple_0 @ E) )  @ A)  &  ( (r1_tarski @  (k10_xtuple_0 @ E) )  @ B) ) ) ) ) ) ) ) ) ) ) , file(funct_2, d2_funct_2)).
thf(commutativity_k2_tarski, axiom,   (! [A: $i, B: $i] :  ( (= @  ( (k2_tarski @ A)  @ B) )  @  ( (k2_tarski @ B)  @ A) ) ) , file(tarski, k2_tarski)).
thf(t23_polyform, conjecture,   (! [A: $i] :  (! [B: $i] :  ( ( ( (m2_funct_2 @  ( ( (k8_funcop_1 @  (u1_struct_0 @ k2_bspace) )  @  ( (k2_zfmisc_1 @ A)  @ B) )  @  (k5_struct_0 @ k2_bspace) ) )  @  ( (k2_zfmisc_1 @ A)  @ B) )  @  ( (k2_tarski @  (k4_struct_0 @ k2_bspace) )  @  (k5_struct_0 @ k2_bspace) ) )  @  ( (k9_funct_2 @  ( (k2_zfmisc_1 @ A)  @ B) )  @  ( (k2_tarski @  (k4_struct_0 @ k2_bspace) )  @  (k5_struct_0 @ k2_bspace) ) ) ) ) ) , file(polyform, t23_polyform)).