include('Axioms/SET010^0.ax').
thf(v1_xboole_0_type, type, v1_xboole_0: $i > $o).
thf(v1_prob_1_type, type, v1_prob_1: $i > $i > $o).
thf(v4_prob_1_type, type, v4_prob_1: $i > $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(v1_funct_1_type, type, v1_funct_1: $i > $o).
thf(k2_zfmisc_1_type, type, k2_zfmisc_1: $i > $i > $i).
thf(k7_numbers_type, type, k7_numbers: $i).
thf(r1_mesfunc2_type, type, r1_mesfunc2: $i > $i > $i > $o).
thf(v4_mesfunc5_type, type, v4_mesfunc5: $i > $o).
thf(v3_mesfunc5_type, type, v3_mesfunc5: $i > $o).
thf(k2_supinf_1_type, type, k2_supinf_1: $i).
thf(k2_xxreal_0_type, type, k2_xxreal_0: $i).
thf(k1_supinf_1_type, type, k1_supinf_1: $i).
thf(k1_xxreal_0_type, type, k1_xxreal_0: $i).
thf(v1_relat_1_type, type, v1_relat_1: $i > $o).
thf(v3_valued_0_type, type, v3_valued_0: $i > $o).
thf(v3_membered_type, type, v3_membered: $i > $o).
thf(k10_xtuple_0_type, type, k10_xtuple_0: $i > $i).
thf(v1_xreal_0_type, type, v1_xreal_0: $i > $o).
thf(v1_prob_2_type, type, v1_prob_2: $i > $o).
thf(m2_finseq_1_type, type, m2_finseq_1: $i > $i > $o).
thf(k1_relset_1_type, type, k1_relset_1: $i > $i > $i).
thf(k3_tarski_type, type, k3_tarski: $i > $i).
thf(k2_relset_1_type, type, k2_relset_1: $i > $i > $i).
thf(v7_ordinal1_type, type, v7_ordinal1: $i > $o).
thf(k4_finseq_1_type, type, k4_finseq_1: $i > $i).
thf(k1_funct_1_type, type, k1_funct_1: $i > $i > $i).
thf(k12_supinf_2_type, type, k12_supinf_2: $i > $i > $i).
thf(t1_subset, axiom,   (! [A: $i] :  (! [B: $i] :  ( ( (r2_hidden @ A)  @ B)  =>  ( (m1_subset_1 @ A)  @ B) ) ) ) , file(subset, t1_subset)).
thf(redefinition_k2_supinf_1, axiom,   ( (= @ k2_supinf_1)  @ k2_xxreal_0) , file(supinf_1, k2_supinf_1)).
thf(redefinition_k1_supinf_1, axiom,   ( (= @ k1_supinf_1)  @ k1_xxreal_0) , file(supinf_1, k1_supinf_1)).
thf(fc3_valued_0, axiom,   (! [A: $i] :  ( ( (v1_relat_1 @ A)  &  (v3_valued_0 @ A) )  =>  (v3_membered @  (k10_xtuple_0 @ A) ) ) ) , file(valued_0, fc3_valued_0)).
thf(fc2_xreal_0, axiom,   ~ ( (v1_xreal_0 @ k1_xxreal_0) ) , file(xreal_0, fc2_xreal_0)).
thf(fc1_xreal_0, axiom,   ~ ( (v1_xreal_0 @ k2_xxreal_0) ) , file(xreal_0, fc1_xreal_0)).
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(d4_mesfunc2, axiom,   (! [A: $i] :  ( ~ ( (v1_xboole_0 @ A) )  =>  (! [B: $i] :  ( ( ~ ( (v1_xboole_0 @ B) )  &  ( ( (v1_prob_1 @ B)  @ A)  &  ( ( (v4_prob_1 @ B)  @ A)  &  ( (m1_subset_1 @ B)  @  (k1_zfmisc_1 @  (k1_zfmisc_1 @ A) ) ) ) ) )  =>  (! [C: $i] :  ( ( (v1_funct_1 @ C)  &  ( (m1_subset_1 @ C)  @  (k1_zfmisc_1 @  ( (k2_zfmisc_1 @ A)  @ k7_numbers) ) ) )  =>  ( ( ( (r1_mesfunc2 @ A)  @ B)  @ C)  <=>  ( (v3_valued_0 @ C)  &  (? [D: $i] :  ( ( (v1_prob_2 @ D)  &  ( (m2_finseq_1 @ D)  @ B) )  &  ( ( (= @  ( (k1_relset_1 @ A)  @ C) )  @  (k3_tarski @  ( (k2_relset_1 @ B)  @ D) ) )  &  (! [E: $i] :  ( (v7_ordinal1 @ E)  =>  (! [F: $i] :  ( ( (m1_subset_1 @ F)  @ A)  =>  (! [G: $i] :  ( ( (m1_subset_1 @ G)  @ A)  =>  ( ( ( (r2_hidden @ E)  @  (k4_finseq_1 @ D) )  &  ( ( (r2_hidden @ F)  @  ( (k1_funct_1 @ D)  @ E) )  &  ( (r2_hidden @ G)  @  ( (k1_funct_1 @ D)  @ E) ) ) )  =>  ( (= @  ( (k12_supinf_2 @ C)  @ F) )  @  ( (k12_supinf_2 @ C)  @ G) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) , file(mesfunc2, d4_mesfunc2)).
thf(d3_mesfunc5, axiom,   (! [A: $i] :  ( (v1_relat_1 @ A)  =>  ( (v3_mesfunc5 @ A)  <=>  ~ ( ( (r2_hidden @ k2_supinf_1)  @  (k10_xtuple_0 @ A) ) ) ) ) ) , file(mesfunc5, d3_mesfunc5)).
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(cc14_membered, axiom,   (! [A: $i] :  ( (v3_membered @ A)  =>  (! [B: $i] :  ( ( (m1_subset_1 @ B)  @ A)  =>  (v1_xreal_0 @ B) ) ) ) ) , file(membered, cc14_membered)).
thf(t14_mesfunc5, conjecture,   (! [A: $i] :  ( ~ ( (v1_xboole_0 @ A) )  =>  (! [B: $i] :  ( ( ~ ( (v1_xboole_0 @ B) )  &  ( ( (v1_prob_1 @ B)  @ A)  &  ( ( (v4_prob_1 @ B)  @ A)  &  ( (m1_subset_1 @ B)  @  (k1_zfmisc_1 @  (k1_zfmisc_1 @ A) ) ) ) ) )  =>  (! [C: $i] :  ( ( (v1_funct_1 @ C)  &  ( (m1_subset_1 @ C)  @  (k1_zfmisc_1 @  ( (k2_zfmisc_1 @ A)  @ k7_numbers) ) ) )  =>  ( ( ( (r1_mesfunc2 @ A)  @ B)  @ C)  =>  ( (v4_mesfunc5 @ C)  &  (v3_mesfunc5 @ C) ) ) ) ) ) ) ) ) , file(mesfunc5, t14_mesfunc5)).