include('Axioms/SET010^0.ax').
thf(v1_xboole_0_type, type, v1_xboole_0: $i > $o).
thf(v1_funct_1_type, type, v1_funct_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(k2_zfmisc_1_type, type, k2_zfmisc_1: $i > $i > $i).
thf(k7_numbers_type, type, k7_numbers: $i).
thf(k1_relset_1_type, type, k1_relset_1: $i > $i > $i).
thf(r1_xxreal_0_type, type, r1_xxreal_0: $i > $i > $o).
thf(k1_supinf_1_type, type, k1_supinf_1: $i).
thf(k12_supinf_2_type, type, k12_supinf_2: $i > $i > $i).
thf(v4_mesfunc5_type, type, v4_mesfunc5: $i > $o).
thf(v1_xxreal_0_type, type, v1_xxreal_0: $i > $o).
thf(k1_xxreal_0_type, type, k1_xxreal_0: $i).
thf(v1_relat_1_type, type, v1_relat_1: $i > $o).
thf(v4_relat_1_type, type, v4_relat_1: $i > $i > $o).
thf(k9_xtuple_0_type, type, k9_xtuple_0: $i > $i).
thf(v2_valued_0_type, type, v2_valued_0: $i > $o).
thf(k1_funct_1_type, type, k1_funct_1: $i > $i > $i).
thf(k10_xtuple_0_type, type, k10_xtuple_0: $i > $i).
thf(v5_relat_1_type, type, v5_relat_1: $i > $i > $o).
thf(t4_xxreal_0, axiom,   (! [A: $i] :  ( (v1_xxreal_0 @ A)  =>  ( ( (r1_xxreal_0 @ k1_xxreal_0)  @ A)  =>  ( (= @ A)  @ k1_xxreal_0) ) ) ) , file(xxreal_0, t4_xxreal_0)).
thf(redefinition_k1_supinf_1, axiom,   ( (= @ k1_supinf_1)  @ k1_xxreal_0) , file(supinf_1, k1_supinf_1)).
thf(redefinition_k1_relset_1, axiom,   (! [A: $i, B: $i] :  ( ( (v1_relat_1 @ B)  &  ( (v4_relat_1 @ B)  @ A) )  =>  ( (= @  ( (k1_relset_1 @ A)  @ B) )  @  (k9_xtuple_0 @ B) ) ) ) , file(relset_1, k1_relset_1)).
thf(redefinition_k12_supinf_2, axiom,   (! [A: $i, B: $i] :  ( ( (v1_relat_1 @ A)  &  ( (v1_funct_1 @ A)  &  (v2_valued_0 @ A) ) )  =>  ( (= @  ( (k12_supinf_2 @ A)  @ B) )  @  ( (k1_funct_1 @ A)  @ B) ) ) ) , file(supinf_2, k12_supinf_2)).
thf(fc62_valued_0, axiom,   (! [A: $i, B: $i] :  ( ( (v1_relat_1 @ A)  &  ( (v1_funct_1 @ A)  &  (v2_valued_0 @ A) ) )  =>  (v1_xxreal_0 @  ( (k1_funct_1 @ A)  @ B) ) ) ) , file(valued_0, fc62_valued_0)).
thf(d6_mesfunc5, axiom,   (! [A: $i] :  ( ~ ( (v1_xboole_0 @ A) )  =>  (! [B: $i] :  ( ( (v1_funct_1 @ B)  &  ( (m1_subset_1 @ B)  @  (k1_zfmisc_1 @  ( (k2_zfmisc_1 @ A)  @ k7_numbers) ) ) )  =>  ( (v4_mesfunc5 @ B)  <=>  (! [C: $i] :  ~ ( ( (r1_xxreal_0 @ k1_supinf_1)  @  ( (k12_supinf_2 @ B)  @ C) ) ) ) ) ) ) ) ) , file(mesfunc5, d6_mesfunc5)).
thf(d4_mesfunc5, axiom,   (! [A: $i] :  ( (v1_relat_1 @ A)  =>  ( (v4_mesfunc5 @ A)  <=>  ~ ( ( (r2_hidden @ k1_supinf_1)  @  (k10_xtuple_0 @ A) ) ) ) ) ) , file(mesfunc5, d4_mesfunc5)).
thf(d3_funct_1, axiom,   (! [A: $i] :  ( ( (v1_relat_1 @ A)  &  (v1_funct_1 @ A) )  =>  (! [B: $i] :  ( ( (= @ B)  @  (k10_xtuple_0 @ A) )  <=>  (! [C: $i] :  ( ( (r2_hidden @ C)  @ B)  <=>  (? [D: $i] :  ( ( (r2_hidden @ D)  @  (k9_xtuple_0 @ A) )  &  ( (= @ C)  @  ( (k1_funct_1 @ A)  @ D) ) ) ) ) ) ) ) ) ) , file(funct_1, d3_funct_1)).
thf(cc2_relset_1, axiom,   (! [A: $i, B: $i] :  (! [C: $i] :  ( ( (m1_subset_1 @ C)  @  (k1_zfmisc_1 @  ( (k2_zfmisc_1 @ A)  @ B) ) )  =>  ( ( (v4_relat_1 @ C)  @ A)  &  ( (v5_relat_1 @ C)  @ B) ) ) ) ) , file(relset_1, cc2_relset_1)).
thf(cc29_valued_0, axiom,   (! [A: $i] :  ( ( (v1_relat_1 @ A)  &  ( (v5_relat_1 @ A)  @ k7_numbers) )  =>  ( (v1_relat_1 @ A)  &  (v2_valued_0 @ A) ) ) ) , file(valued_0, cc29_valued_0)).
thf(cc1_relset_1, axiom,   (! [A: $i, B: $i] :  (! [C: $i] :  ( ( (m1_subset_1 @ C)  @  (k1_zfmisc_1 @  ( (k2_zfmisc_1 @ A)  @ B) ) )  =>  (v1_relat_1 @ C) ) ) ) , file(relset_1, cc1_relset_1)).
thf(t11_mesfunc5, conjecture,   (! [A: $i] :  ( ~ ( (v1_xboole_0 @ A) )  =>  (! [B: $i] :  ( ( (v1_funct_1 @ B)  &  ( (m1_subset_1 @ B)  @  (k1_zfmisc_1 @  ( (k2_zfmisc_1 @ A)  @ k7_numbers) ) ) )  =>  ( (! [C: $i] :  ~ ( ( ( (r2_hidden @ C)  @  ( (k1_relset_1 @ A)  @ B) )  &  ( (r1_xxreal_0 @ k1_supinf_1)  @  ( (k12_supinf_2 @ B)  @ C) ) ) ) )  <=>  (v4_mesfunc5 @ B) ) ) ) ) ) , file(mesfunc5, t11_mesfunc5)).