include('Axioms/SET010^0.ax').
thf(m1_qc_lang1_type, type, m1_qc_lang1: $i > $o).
thf(k9_substut1_type, type, k9_substut1: $i > $i > $i).
thf(k5_cqc_lang_type, type, k5_cqc_lang: $i > $i).
thf(k1_xboole_0_type, type, k1_xboole_0: $i).
thf(m1_subset_1_type, type, m1_subset_1: $i > $i > $o).
thf(k9_qc_lang1_type, type, k9_qc_lang1: $i > $i).
thf(k1_subset_1_type, type, k1_subset_1: $i > $i).
thf(k3_qc_lang1_type, type, k3_qc_lang1: $i > $i).
thf(v2_qc_lang1_type, type, v2_qc_lang1: $i > $i > $o).
thf(k8_substut1_type, type, k8_substut1: $i > $i > $i).
thf(k17_qc_lang1_type, type, k17_qc_lang1: $i > $i > $i).
thf(v3_qc_lang1_type, type, v3_qc_lang1: $i > $i > $o).
thf(k18_qc_lang1_type, type, k18_qc_lang1: $i > $i > $i).
thf(v4_qc_lang1_type, type, v4_qc_lang1: $i > $i > $o).
thf(k4_subset_1_type, type, k4_subset_1: $i > $i > $i > $i).
thf(k19_qc_lang1_type, type, k19_qc_lang1: $i > $i > $i).
thf(k20_qc_lang1_type, type, k20_qc_lang1: $i > $i > $i).
thf(v5_qc_lang1_type, type, v5_qc_lang1: $i > $i > $o).
thf(k22_qc_lang1_type, type, k22_qc_lang1: $i > $i > $i).
thf(k6_domain_1_type, type, k6_domain_1: $i > $i > $i).
thf(k21_qc_lang1_type, type, k21_qc_lang1: $i > $i > $i).
thf(v1_xboole_0_type, type, v1_xboole_0: $i > $o).
thf(l10_substut1, axiom,   (! [A: $i] :  ( (m1_qc_lang1 @ A)  =>  (! [B: $i] :  ( ( (m1_subset_1 @ B)  @  (k9_qc_lang1 @ A) )  =>  ( ( (= @  ( (k9_substut1 @ A)  @  (k5_cqc_lang @ A) ) )  @  (k1_subset_1 @  (k3_qc_lang1 @ A) ) )  &  ( ( ( (v2_qc_lang1 @ B)  @ A)  =>  ( (= @  ( (k9_substut1 @ A)  @ B) )  @  ( (k8_substut1 @ A)  @  ( (k17_qc_lang1 @ A)  @ B) ) ) )  &  ( ( ( (v3_qc_lang1 @ B)  @ A)  =>  ( (= @  ( (k9_substut1 @ A)  @ B) )  @  ( (k9_substut1 @ A)  @  ( (k18_qc_lang1 @ A)  @ B) ) ) )  &  ( ( ( (v4_qc_lang1 @ B)  @ A)  =>  ( (= @  ( (k9_substut1 @ A)  @ B) )  @  ( ( (k4_subset_1 @  (k3_qc_lang1 @ A) )  @  ( (k9_substut1 @ A)  @  ( (k19_qc_lang1 @ A)  @ B) ) )  @  ( (k9_substut1 @ A)  @  ( (k20_qc_lang1 @ A)  @ B) ) ) ) )  &  ( ( (v5_qc_lang1 @ B)  @ A)  =>  ( (= @  ( (k9_substut1 @ A)  @ B) )  @  ( ( (k4_subset_1 @  (k3_qc_lang1 @ A) )  @  ( (k9_substut1 @ A)  @  ( (k22_qc_lang1 @ A)  @ B) ) )  @  ( (k6_domain_1 @  (k3_qc_lang1 @ A) )  @  ( (k21_qc_lang1 @ A)  @ B) ) ) ) ) ) ) ) ) ) ) ) ) , file(substut1, l10_substut1)).
thf(existence_m1_subset_1, axiom,   (! [A: $i] :  (? [B: $i] :  ( (m1_subset_1 @ B)  @ A) ) ) , file(subset_1, m1_subset_1)).
thf(d2_xboole_0, axiom,   ( (= @ k1_xboole_0)  @  (eps @  (^ [A: $i] :  (v1_xboole_0 @ A) ) ) ) , file(xboole_0, d2_xboole_0)).
thf(d2_subset_1, axiom,   (! [A: $i] :  ( (= @  (k1_subset_1 @ A) )  @ k1_xboole_0) ) , file(subset_1, d2_subset_1)).
thf(t2_substut1, conjecture,   (! [A: $i] :  ( (m1_qc_lang1 @ A)  =>  ( (= @  ( (k9_substut1 @ A)  @  (k5_cqc_lang @ A) ) )  @ k1_xboole_0) ) ) , file(substut1, t2_substut1)).