include('Axioms/SET010^0.ax').
thf(v2_struct_0_type, type, v2_struct_0: $i > $o).
thf(v13_algstr_0_type, type, v13_algstr_0: $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(l1_rlvect_1_type, type, l1_rlvect_1: $i > $o).
thf(m1_subset_1_type, type, m1_subset_1: $i > $i > $o).
thf(k1_zfmisc_1_type, type, k1_zfmisc_1: $i > $i).
thf(u1_struct_0_type, type, u1_struct_0: $i > $i).
thf(k4_struct_0_type, type, k4_struct_0: $i > $i).
thf(r1_tarski_type, type, r1_tarski: $i > $i > $o).
thf(k3_mathmorp_type, type, k3_mathmorp: $i > $i > $i > $i).
thf(k6_rusub_4_type, type, k6_rusub_4: $i > $i > $i > $i).
thf(v1_xboole_0_type, type, v1_xboole_0: $i > $o).
thf(k6_domain_1_type, type, k6_domain_1: $i > $i > $i).
thf(k1_tarski_type, type, k1_tarski: $i > $i).
thf(l2_algstr_0_type, type, l2_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(t7_boole, axiom,   (! [A: $i] :  (! [B: $i] :  ~ ( ( ( (r2_hidden @ A)  @ B)  &  (v1_xboole_0 @ B) ) ) ) ) , file(boole, t7_boole)).
thf(t5_mathmorp, axiom,   (! [A: $i] :  ( ( ~ ( (v2_struct_0 @ A) )  &  ( (v13_algstr_0 @ A)  &  ( (v2_rlvect_1 @ A)  &  ( (v3_rlvect_1 @ A)  &  ( (v4_rlvect_1 @ A)  &  (l1_rlvect_1 @ A) ) ) ) ) )  =>  (! [B: $i] :  ( ( (m1_subset_1 @ B)  @  (k1_zfmisc_1 @  (u1_struct_0 @ A) ) )  =>  ( (= @  ( ( (k3_mathmorp @ A)  @ B)  @  ( (k6_domain_1 @  (u1_struct_0 @ A) )  @  (k4_struct_0 @ A) ) ) )  @ B) ) ) ) ) , file(mathmorp, t5_mathmorp)).
thf(t31_zfmisc_1, axiom,   (! [A: $i] :  (! [B: $i] :  ( ( (r1_tarski @  (k1_tarski @ A) )  @ B)  <=>  ( (r2_hidden @ A)  @ B) ) ) ) , file(zfmisc_1, t31_zfmisc_1)).
thf(t12_rltopsp1, axiom,   (! [A: $i] :  ( ( ~ ( (v2_struct_0 @ A) )  &  ( (v4_rlvect_1 @ A)  &  (l2_algstr_0 @ A) ) )  =>  (! [B: $i] :  ( ( (m1_subset_1 @ B)  @  (k1_zfmisc_1 @  (u1_struct_0 @ A) ) )  =>  (! [C: $i] :  ( ( (m1_subset_1 @ C)  @  (k1_zfmisc_1 @  (u1_struct_0 @ A) ) )  =>  ( ( (r2_hidden @  (k4_struct_0 @ A) )  @ C)  =>  ( (r1_tarski @ B)  @  ( ( (k6_rusub_4 @ A)  @ B)  @ C) ) ) ) ) ) ) ) ) , file(rltopsp1, t12_rltopsp1)).
thf(t10_mathmorp, axiom,   (! [A: $i] :  ( ( ~ ( (v2_struct_0 @ A) )  &  ( (v13_algstr_0 @ A)  &  ( (v2_rlvect_1 @ A)  &  ( (v3_rlvect_1 @ A)  &  ( (v4_rlvect_1 @ A)  &  (l1_rlvect_1 @ A) ) ) ) ) )  =>  (! [B: $i] :  ( ( (m1_subset_1 @ B)  @  (k1_zfmisc_1 @  (u1_struct_0 @ A) ) )  =>  (! [C: $i] :  ( ( (m1_subset_1 @ C)  @  (k1_zfmisc_1 @  (u1_struct_0 @ A) ) )  =>  (! [D: $i] :  ( ( (m1_subset_1 @ D)  @  (k1_zfmisc_1 @  (u1_struct_0 @ A) ) )  =>  ( ( (r1_tarski @ B)  @ C)  =>  ( ( (r1_tarski @  ( ( (k3_mathmorp @ A)  @ D)  @ C) )  @  ( ( (k3_mathmorp @ A)  @ D)  @ B) )  &  ( (r1_tarski @  ( ( (k6_rusub_4 @ A)  @ D)  @ B) )  @  ( ( (k6_rusub_4 @ A)  @ D)  @ C) ) ) ) ) ) ) ) ) ) ) ) , file(mathmorp, t10_mathmorp)).
thf(redefinition_k6_domain_1, axiom,   (! [A: $i, B: $i] :  ( ( ~ ( (v1_xboole_0 @ A) )  &  ( (m1_subset_1 @ B)  @ A) )  =>  ( (= @  ( (k6_domain_1 @ A)  @ B) )  @  (k1_tarski @ B) ) ) ) , file(domain_1, k6_domain_1)).
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_l1_rlvect_1, axiom,   (! [A: $i] :  ( (l1_rlvect_1 @ A)  =>  (l2_algstr_0 @ A) ) ) , file(rlvect_1, l1_rlvect_1)).
thf(dt_k6_domain_1, axiom,   (! [A: $i, B: $i] :  ( ( ~ ( (v1_xboole_0 @ A) )  &  ( (m1_subset_1 @ B)  @ A) )  =>  ( (m1_subset_1 @  ( (k6_domain_1 @ A)  @ B) )  @  (k1_zfmisc_1 @ A) ) ) ) , file(domain_1, k6_domain_1)).
thf(dt_k4_struct_0, axiom,   (! [A: $i] :  ( (l2_struct_0 @ A)  =>  ( (m1_subset_1 @  (k4_struct_0 @ A) )  @  (u1_struct_0 @ A) ) ) ) , file(struct_0, k4_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(t11_mathmorp, conjecture,   (! [A: $i] :  ( ( ~ ( (v2_struct_0 @ A) )  &  ( (v13_algstr_0 @ A)  &  ( (v2_rlvect_1 @ A)  &  ( (v3_rlvect_1 @ A)  &  ( (v4_rlvect_1 @ A)  &  (l1_rlvect_1 @ A) ) ) ) ) )  =>  (! [B: $i] :  ( ( (m1_subset_1 @ B)  @  (k1_zfmisc_1 @  (u1_struct_0 @ A) ) )  =>  (! [C: $i] :  ( ( (m1_subset_1 @ C)  @  (k1_zfmisc_1 @  (u1_struct_0 @ A) ) )  =>  ( ( (r2_hidden @  (k4_struct_0 @ A) )  @ B)  =>  ( ( (r1_tarski @  ( ( (k3_mathmorp @ A)  @ C)  @ B) )  @ C)  &  ( (r1_tarski @ C)  @  ( ( (k6_rusub_4 @ A)  @ C)  @ B) ) ) ) ) ) ) ) ) ) , file(mathmorp, t11_mathmorp)).