include('Axioms/product_2.ax').
tff(tp_c_2Emeasure_2EBorel,type,(c_2Emeasure_2EBorel:$i)).
tff(mem_c_2Emeasure_2EBorel,axiom,mem(c_2Emeasure_2EBorel,ty_2Epair_2Eprod(arr(ty_2Eextreal_2Eextreal,bool),arr(arr(ty_2Eextreal_2Eextreal,bool),bool)))).
tff(tp_c_2Emeasure_2Eadditive,type,(c_2Emeasure_2Eadditive:del > $i)).
tff(mem_c_2Emeasure_2Eadditive,axiom,( ! [A_27a:del] : mem(c_2Emeasure_2Eadditive(A_27a),arr(ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))),bool)))).
tff(tp_c_2Emeasure_2Ealgebra,type,(c_2Emeasure_2Ealgebra:del > $i)).
tff(mem_c_2Emeasure_2Ealgebra,axiom,( ! [A_27a:del] : mem(c_2Emeasure_2Ealgebra(A_27a),arr(ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool)),bool)))).
tff(tp_c_2Emeasure_2Eclosed__cdi,type,(c_2Emeasure_2Eclosed__cdi:del > $i)).
tff(mem_c_2Emeasure_2Eclosed__cdi,axiom,( ! [A_27a:del] : mem(c_2Emeasure_2Eclosed__cdi(A_27a),arr(ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool)),bool)))).
tff(tp_c_2Emeasure_2Ecountably__additive,type,(c_2Emeasure_2Ecountably__additive:del > $i)).
tff(mem_c_2Emeasure_2Ecountably__additive,axiom,( ! [A_27a:del] : mem(c_2Emeasure_2Ecountably__additive(A_27a),arr(ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))),bool)))).
tff(tp_c_2Emeasure_2Ecountably__subadditive,type,(c_2Emeasure_2Ecountably__subadditive:del > $i)).
tff(mem_c_2Emeasure_2Ecountably__subadditive,axiom,( ! [A_27a:del] : mem(c_2Emeasure_2Ecountably__subadditive(A_27a),arr(ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))),bool)))).
tff(tp_c_2Emeasure_2Efn__abs,type,(c_2Emeasure_2Efn__abs:del > $i)).
tff(mem_c_2Emeasure_2Efn__abs,axiom,( ! [A_27a:del] : mem(c_2Emeasure_2Efn__abs(A_27a),arr(arr(A_27a,ty_2Eextreal_2Eextreal),arr(A_27a,ty_2Eextreal_2Eextreal))))).
tff(tp_c_2Emeasure_2Efn__minus,type,(c_2Emeasure_2Efn__minus:del > $i)).
tff(mem_c_2Emeasure_2Efn__minus,axiom,( ! [A_27a:del] : mem(c_2Emeasure_2Efn__minus(A_27a),arr(arr(A_27a,ty_2Eextreal_2Eextreal),arr(A_27a,ty_2Eextreal_2Eextreal))))).
tff(tp_c_2Emeasure_2Efn__plus,type,(c_2Emeasure_2Efn__plus:del > $i)).
tff(mem_c_2Emeasure_2Efn__plus,axiom,( ! [A_27a:del] : mem(c_2Emeasure_2Efn__plus(A_27a),arr(arr(A_27a,ty_2Eextreal_2Eextreal),arr(A_27a,ty_2Eextreal_2Eextreal))))).
tff(tp_c_2Emeasure_2Eincreasing,type,(c_2Emeasure_2Eincreasing:del > $i)).
tff(mem_c_2Emeasure_2Eincreasing,axiom,( ! [A_27a:del] : mem(c_2Emeasure_2Eincreasing(A_27a),arr(ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))),bool)))).
tff(tp_c_2Emeasure_2Eindicator__fn,type,(c_2Emeasure_2Eindicator__fn:del > $i)).
tff(mem_c_2Emeasure_2Eindicator__fn,axiom,( ! [A_27a:del] : mem(c_2Emeasure_2Eindicator__fn(A_27a),arr(arr(A_27a,bool),arr(A_27a,ty_2Eextreal_2Eextreal))))).
tff(tp_c_2Emeasure_2Einf__measure,type,(c_2Emeasure_2Einf__measure:del > $i)).
tff(mem_c_2Emeasure_2Einf__measure,axiom,( ! [A_27a:del] : mem(c_2Emeasure_2Einf__measure(A_27a),arr(ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))))).
tff(tp_c_2Emeasure_2Elambda__system,type,(c_2Emeasure_2Elambda__system:del > $i)).
tff(mem_c_2Emeasure_2Elambda__system,axiom,( ! [A_27a:del] : mem(c_2Emeasure_2Elambda__system(A_27a),arr(ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool)),arr(arr(arr(A_27a,bool),ty_2Erealax_2Ereal),arr(arr(A_27a,bool),bool)))))).
tff(tp_c_2Emeasure_2Em__space,type,(c_2Emeasure_2Em__space:del > $i)).
tff(mem_c_2Emeasure_2Em__space,axiom,( ! [A_27a:del] : mem(c_2Emeasure_2Em__space(A_27a),arr(ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))),arr(A_27a,bool))))).
tff(tp_c_2Emeasure_2Emeasurable,type,(c_2Emeasure_2Emeasurable:(del * del) > $i)).
tff(mem_c_2Emeasure_2Emeasurable,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Emeasure_2Emeasurable(A_27a,A_27b),arr(ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool)),arr(ty_2Epair_2Eprod(arr(A_27b,bool),arr(arr(A_27b,bool),bool)),arr(arr(A_27a,A_27b),bool))))))).
tff(tp_c_2Emeasure_2Emeasurable__sets,type,(c_2Emeasure_2Emeasurable__sets:del > $i)).
tff(mem_c_2Emeasure_2Emeasurable__sets,axiom,( ! [A_27a:del] : mem(c_2Emeasure_2Emeasurable__sets(A_27a),arr(ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))),arr(arr(A_27a,bool),bool))))).
tff(tp_c_2Emeasure_2Emeasure,type,(c_2Emeasure_2Emeasure:del > $i)).
tff(mem_c_2Emeasure_2Emeasure,axiom,( ! [A_27a:del] : mem(c_2Emeasure_2Emeasure(A_27a),arr(ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))))).
tff(tp_c_2Emeasure_2Emeasure__preserving,type,(c_2Emeasure_2Emeasure__preserving:(del * del) > $i)).
tff(mem_c_2Emeasure_2Emeasure__preserving,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Emeasure_2Emeasure__preserving(A_27a,A_27b),arr(ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))),arr(ty_2Epair_2Eprod(arr(A_27b,bool),ty_2Epair_2Eprod(arr(arr(A_27b,bool),bool),arr(arr(A_27b,bool),ty_2Erealax_2Ereal))),arr(arr(A_27a,A_27b),bool))))))).
tff(tp_c_2Emeasure_2Emeasure__space,type,(c_2Emeasure_2Emeasure__space:del > $i)).
tff(mem_c_2Emeasure_2Emeasure__space,axiom,( ! [A_27a:del] : mem(c_2Emeasure_2Emeasure__space(A_27a),arr(ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))),bool)))).
tff(tp_c_2Emeasure_2Enull__set,type,(c_2Emeasure_2Enull__set:del > $i)).
tff(mem_c_2Emeasure_2Enull__set,axiom,( ! [A_27a:del] : mem(c_2Emeasure_2Enull__set(A_27a),arr(ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))),arr(arr(A_27a,bool),bool))))).
tff(tp_c_2Emeasure_2Eouter__measure__space,type,(c_2Emeasure_2Eouter__measure__space:del > $i)).
tff(mem_c_2Emeasure_2Eouter__measure__space,axiom,( ! [A_27a:del] : mem(c_2Emeasure_2Eouter__measure__space(A_27a),arr(ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))),bool)))).
tff(tp_c_2Emeasure_2Epos__simple__fn,type,(c_2Emeasure_2Epos__simple__fn:del > $i)).
tff(mem_c_2Emeasure_2Epos__simple__fn,axiom,( ! [A_27a:del] : mem(c_2Emeasure_2Epos__simple__fn(A_27a),arr(ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))),arr(arr(A_27a,ty_2Eextreal_2Eextreal),arr(arr(ty_2Enum_2Enum,bool),arr(arr(ty_2Enum_2Enum,arr(A_27a,bool)),arr(arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal),bool)))))))).
tff(tp_c_2Emeasure_2Epositive,type,(c_2Emeasure_2Epositive:del > $i)).
tff(mem_c_2Emeasure_2Epositive,axiom,( ! [A_27a:del] : mem(c_2Emeasure_2Epositive(A_27a),arr(ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))),bool)))).
tff(tp_c_2Emeasure_2Esigma,type,(c_2Emeasure_2Esigma:del > $i)).
tff(mem_c_2Emeasure_2Esigma,axiom,( ! [A_27a:del] : mem(c_2Emeasure_2Esigma(A_27a),arr(arr(A_27a,bool),arr(arr(arr(A_27a,bool),bool),ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool))))))).
tff(tp_c_2Emeasure_2Esigma__algebra,type,(c_2Emeasure_2Esigma__algebra:del > $i)).
tff(mem_c_2Emeasure_2Esigma__algebra,axiom,( ! [A_27a:del] : mem(c_2Emeasure_2Esigma__algebra(A_27a),arr(ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool)),bool)))).
tff(tp_c_2Emeasure_2Esmallest__closed__cdi,type,(c_2Emeasure_2Esmallest__closed__cdi:del > $i)).
tff(mem_c_2Emeasure_2Esmallest__closed__cdi,axiom,( ! [A_27a:del] : mem(c_2Emeasure_2Esmallest__closed__cdi(A_27a),arr(ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool)),ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool)))))).
tff(tp_c_2Emeasure_2Espace,type,(c_2Emeasure_2Espace:del > $i)).
tff(mem_c_2Emeasure_2Espace,axiom,( ! [A_27a:del] : mem(c_2Emeasure_2Espace(A_27a),arr(ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool)),arr(A_27a,bool))))).
tff(tp_c_2Emeasure_2Esubadditive,type,(c_2Emeasure_2Esubadditive:del > $i)).
tff(mem_c_2Emeasure_2Esubadditive,axiom,( ! [A_27a:del] : mem(c_2Emeasure_2Esubadditive(A_27a),arr(ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))),bool)))).
tff(tp_c_2Emeasure_2Esubset__class,type,(c_2Emeasure_2Esubset__class:del > $i)).
tff(mem_c_2Emeasure_2Esubset__class,axiom,( ! [A_27a:del] : mem(c_2Emeasure_2Esubset__class(A_27a),arr(arr(A_27a,bool),arr(arr(arr(A_27a,bool),bool),bool))))).
tff(tp_c_2Emeasure_2Esubsets,type,(c_2Emeasure_2Esubsets:del > $i)).
tff(mem_c_2Emeasure_2Esubsets,axiom,( ! [A_27a:del] : mem(c_2Emeasure_2Esubsets(A_27a),arr(ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool)),arr(arr(A_27a,bool),bool))))).
tff(ax_thm_2Emeasure_2Espace__def,axiom,( ! [A_27a:del]: ( ! [V0x:$i] : (mem(V0x,arr(A_27a,bool)) => ( ! [V1y:$i] : (mem(V1y,arr(arr(A_27a,bool),bool)) => (ap(c_2Emeasure_2Espace(A_27a),ap(ap(c_2Epair_2E_2C(arr(A_27a,bool),arr(arr(A_27a,bool),bool)),V0x),V1y)) = V0x))))))).
tff(ax_thm_2Emeasure_2Esubsets__def,axiom,( ! [A_27a:del]: ( ! [V0x:$i] : (mem(V0x,arr(A_27a,bool)) => ( ! [V1y:$i] : (mem(V1y,arr(arr(A_27a,bool),bool)) => (ap(c_2Emeasure_2Esubsets(A_27a),ap(ap(c_2Epair_2E_2C(arr(A_27a,bool),arr(arr(A_27a,bool),bool)),V0x),V1y)) = V1y))))))).
tff(ax_thm_2Emeasure_2Esubset__class__def,axiom,( ! [A_27a:del]: ( ! [V0sp:$i] : (mem(V0sp,arr(A_27a,bool)) => ( ! [V1sts:$i] : (mem(V1sts,arr(arr(A_27a,bool),bool)) => (p(ap(ap(c_2Emeasure_2Esubset__class(A_27a),V0sp),V1sts)) <=> ( ! [V2x:$i] : (mem(V2x,arr(A_27a,bool)) => (p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V2x),V1sts)) => p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),V2x),V0sp)))))))))))).
tff(ax_thm_2Emeasure_2Ealgebra__def,axiom,( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool))) => (p(ap(c_2Emeasure_2Ealgebra(A_27a),V0a)) <=> (p(ap(ap(c_2Emeasure_2Esubset__class(A_27a),ap(c_2Emeasure_2Espace(A_27a),V0a)),ap(c_2Emeasure_2Esubsets(A_27a),V0a))) & (p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),c_2Epred__set_2EEMPTY(A_27a)),ap(c_2Emeasure_2Esubsets(A_27a),V0a))) & (( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => (p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V1s),ap(c_2Emeasure_2Esubsets(A_27a),V0a))) => p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),ap(ap(c_2Epred__set_2EDIFF(A_27a),ap(c_2Emeasure_2Espace(A_27a),V0a)),V1s)),ap(c_2Emeasure_2Esubsets(A_27a),V0a)))))) & ( ! [V2s:$i] : (mem(V2s,arr(A_27a,bool)) => ( ! [V3t:$i] : (mem(V3t,arr(A_27a,bool)) => ((p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V2s),ap(c_2Emeasure_2Esubsets(A_27a),V0a))) & p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V3t),ap(c_2Emeasure_2Esubsets(A_27a),V0a)))) => p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),ap(ap(c_2Epred__set_2EUNION(A_27a),V2s),V3t)),ap(c_2Emeasure_2Esubsets(A_27a),V0a)))))))))))))))).
tff(ax_thm_2Emeasure_2Esigma__algebra__def,axiom,( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool))) => (p(ap(c_2Emeasure_2Esigma__algebra(A_27a),V0a)) <=> (p(ap(c_2Emeasure_2Ealgebra(A_27a),V0a)) & ( ! [V1c:$i] : (mem(V1c,arr(arr(A_27a,bool),bool)) => ((p(ap(c_2Epred__set_2Ecountable(arr(A_27a,bool)),V1c)) & p(ap(ap(c_2Epred__set_2ESUBSET(arr(A_27a,bool)),V1c),ap(c_2Emeasure_2Esubsets(A_27a),V0a)))) => p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),ap(c_2Epred__set_2EBIGUNION(A_27a),V1c)),ap(c_2Emeasure_2Esubsets(A_27a),V0a)))))))))))).
tff(ax_thm_2Emeasure_2Esigma__def,axiom,( ! [A_27a:del]: ( ! [V0sp:$i] : (mem(V0sp,arr(A_27a,bool)) => ( ! [V1st:$i] : (mem(V1st,arr(arr(A_27a,bool),bool)) => (ap(ap(c_2Emeasure_2Esigma(A_27a),V0sp),V1st) = ap(ap(c_2Epair_2E_2C(arr(A_27a,bool),arr(arr(A_27a,bool),bool)),V0sp),ap(c_2Epred__set_2EBIGINTER(arr(A_27a,bool)),ap(c_2Epred__set_2EGSPEC(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),bool)),f3504(A_27a,V0sp,V1st))))))))))).
tff(ax_thm_2Emeasure_2Em__space__def,axiom,( ! [A_27a:del]: ( ! [V0sp:$i] : (mem(V0sp,arr(A_27a,bool)) => ( ! [V1sts:$i] : (mem(V1sts,arr(arr(A_27a,bool),bool)) => ( ! [V2mu:$i] : (mem(V2mu,arr(arr(A_27a,bool),ty_2Erealax_2Ereal)) => (ap(c_2Emeasure_2Em__space(A_27a),ap(ap(c_2Epair_2E_2C(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))),V0sp),ap(ap(c_2Epair_2E_2C(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)),V1sts),V2mu))) = V0sp))))))))).
tff(ax_thm_2Emeasure_2Emeasurable__sets__def,axiom,( ! [A_27a:del]: ( ! [V0sp:$i] : (mem(V0sp,arr(A_27a,bool)) => ( ! [V1sts:$i] : (mem(V1sts,arr(arr(A_27a,bool),bool)) => ( ! [V2mu:$i] : (mem(V2mu,arr(arr(A_27a,bool),ty_2Erealax_2Ereal)) => (ap(c_2Emeasure_2Emeasurable__sets(A_27a),ap(ap(c_2Epair_2E_2C(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))),V0sp),ap(ap(c_2Epair_2E_2C(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)),V1sts),V2mu))) = V1sts))))))))).
tff(ax_thm_2Emeasure_2Emeasure__def,axiom,( ! [A_27a:del]: ( ! [V0sp:$i] : (mem(V0sp,arr(A_27a,bool)) => ( ! [V1sts:$i] : (mem(V1sts,arr(arr(A_27a,bool),bool)) => ( ! [V2mu:$i] : (mem(V2mu,arr(arr(A_27a,bool),ty_2Erealax_2Ereal)) => (ap(c_2Emeasure_2Emeasure(A_27a),ap(ap(c_2Epair_2E_2C(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))),V0sp),ap(ap(c_2Epair_2E_2C(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)),V1sts),V2mu))) = V2mu))))))))).
tff(ax_thm_2Emeasure_2Epositive__def,axiom,( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => (p(ap(c_2Emeasure_2Epositive(A_27a),V0m)) <=> ((surj__ty_2Erealax_2Ereal(ap(ap(c_2Emeasure_2Emeasure(A_27a),V0m),c_2Epred__set_2EEMPTY(A_27a))) = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) & ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => (p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V1s),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m))) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(ap(c_2Emeasure_2Emeasure(A_27a),V0m),V1s)))))))))))).
tff(ax_thm_2Emeasure_2Eadditive__def,axiom,( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => (p(ap(c_2Emeasure_2Eadditive(A_27a),V0m)) <=> ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => ( ! [V2t:$i] : (mem(V2t,arr(A_27a,bool)) => ((p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V1s),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m))) & (p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V2t),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m))) & p(ap(ap(c_2Epred__set_2EDISJOINT(A_27a),V1s),V2t)))) => (surj__ty_2Erealax_2Ereal(ap(ap(c_2Emeasure_2Emeasure(A_27a),V0m),ap(ap(c_2Epred__set_2EUNION(A_27a),V1s),V2t))) = surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Emeasure_2Emeasure(A_27a),V0m),V1s)),ap(ap(c_2Emeasure_2Emeasure(A_27a),V0m),V2t)))))))))))))).
tff(ax_thm_2Emeasure_2Ecountably__additive__def,axiom,( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => (p(ap(c_2Emeasure_2Ecountably__additive(A_27a),V0m)) <=> ( ! [V1f:$i] : (mem(V1f,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ((p(ap(ap(c_2Ebool_2EIN(arr(ty_2Enum_2Enum,arr(A_27a,bool))),V1f),ap(ap(c_2Epred__set_2EFUNSET(ty_2Enum_2Enum,arr(A_27a,bool)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m)))) & (( ! [V2m:tp__ty_2Enum_2Enum] : ( ! [V3n:tp__ty_2Enum_2Enum] : ((~~ (V2m = V3n)) => p(ap(ap(c_2Epred__set_2EDISJOINT(A_27a),ap(V1f,inj__ty_2Enum_2Enum(V2m))),ap(V1f,inj__ty_2Enum_2Enum(V3n))))))) & p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),ap(c_2Epred__set_2EBIGUNION(A_27a),ap(ap(c_2Epred__set_2EIMAGE(ty_2Enum_2Enum,arr(A_27a,bool)),V1f),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)))),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m))))) => p(ap(ap(c_2Eseq_2Esums,ap(ap(c_2Ecombin_2Eo(ty_2Enum_2Enum,ty_2Erealax_2Ereal,arr(A_27a,bool)),ap(c_2Emeasure_2Emeasure(A_27a),V0m)),V1f)),ap(ap(c_2Emeasure_2Emeasure(A_27a),V0m),ap(c_2Epred__set_2EBIGUNION(A_27a),ap(ap(c_2Epred__set_2EIMAGE(ty_2Enum_2Enum,arr(A_27a,bool)),V1f),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)))))))))))))).
tff(ax_thm_2Emeasure_2Esubadditive__def,axiom,( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => (p(ap(c_2Emeasure_2Esubadditive(A_27a),V0m)) <=> ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => ( ! [V2t:$i] : (mem(V2t,arr(A_27a,bool)) => ((p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V1s),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m))) & p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V2t),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m)))) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Emeasure_2Emeasure(A_27a),V0m),ap(ap(c_2Epred__set_2EUNION(A_27a),V1s),V2t))),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Emeasure_2Emeasure(A_27a),V0m),V1s)),ap(ap(c_2Emeasure_2Emeasure(A_27a),V0m),V2t)))))))))))))).
tff(ax_thm_2Emeasure_2Ecountably__subadditive__def,axiom,( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => (p(ap(c_2Emeasure_2Ecountably__subadditive(A_27a),V0m)) <=> ( ! [V1f:$i] : (mem(V1f,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ((p(ap(ap(c_2Ebool_2EIN(arr(ty_2Enum_2Enum,arr(A_27a,bool))),V1f),ap(ap(c_2Epred__set_2EFUNSET(ty_2Enum_2Enum,arr(A_27a,bool)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m)))) & (p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),ap(c_2Epred__set_2EBIGUNION(A_27a),ap(ap(c_2Epred__set_2EIMAGE(ty_2Enum_2Enum,arr(A_27a,bool)),V1f),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)))),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m))) & p(ap(c_2Eseq_2Esummable,ap(ap(c_2Ecombin_2Eo(ty_2Enum_2Enum,ty_2Erealax_2Ereal,arr(A_27a,bool)),ap(c_2Emeasure_2Emeasure(A_27a),V0m)),V1f))))) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Emeasure_2Emeasure(A_27a),V0m),ap(c_2Epred__set_2EBIGUNION(A_27a),ap(ap(c_2Epred__set_2EIMAGE(ty_2Enum_2Enum,arr(A_27a,bool)),V1f),c_2Epred__set_2EUNIV(ty_2Enum_2Enum))))),ap(c_2Eseq_2Esuminf,ap(ap(c_2Ecombin_2Eo(ty_2Enum_2Enum,ty_2Erealax_2Ereal,arr(A_27a,bool)),ap(c_2Emeasure_2Emeasure(A_27a),V0m)),V1f)))))))))))).
tff(ax_thm_2Emeasure_2Eincreasing__def,axiom,( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => (p(ap(c_2Emeasure_2Eincreasing(A_27a),V0m)) <=> ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => ( ! [V2t:$i] : (mem(V2t,arr(A_27a,bool)) => ((p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V1s),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m))) & (p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V2t),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m))) & p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),V1s),V2t)))) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Emeasure_2Emeasure(A_27a),V0m),V1s)),ap(ap(c_2Emeasure_2Emeasure(A_27a),V0m),V2t))))))))))))).
tff(ax_thm_2Emeasure_2Emeasure__space__def,axiom,( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => (p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) <=> (p(ap(c_2Emeasure_2Esigma__algebra(A_27a),ap(ap(c_2Epair_2E_2C(arr(A_27a,bool),arr(arr(A_27a,bool),bool)),ap(c_2Emeasure_2Em__space(A_27a),V0m)),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m)))) & (p(ap(c_2Emeasure_2Epositive(A_27a),V0m)) & p(ap(c_2Emeasure_2Ecountably__additive(A_27a),V0m))))))))).
tff(ax_thm_2Emeasure_2Elambda__system__def,axiom,( ! [A_27a:del]: ( ! [V0gen:$i] : (mem(V0gen,ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool))) => ( ! [V1lam:$i] : (mem(V1lam,arr(arr(A_27a,bool),ty_2Erealax_2Ereal)) => (ap(ap(c_2Emeasure_2Elambda__system(A_27a),V0gen),V1lam) = ap(c_2Epred__set_2EGSPEC(arr(A_27a,bool),arr(A_27a,bool)),f3506(A_27a,V0gen,V1lam))))))))).
tff(ax_thm_2Emeasure_2Eouter__measure__space__def,axiom,( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => (p(ap(c_2Emeasure_2Eouter__measure__space(A_27a),V0m)) <=> (p(ap(c_2Emeasure_2Epositive(A_27a),V0m)) & (p(ap(c_2Emeasure_2Eincreasing(A_27a),V0m)) & p(ap(c_2Emeasure_2Ecountably__subadditive(A_27a),V0m))))))))).
tff(ax_thm_2Emeasure_2Einf__measure__def,axiom,( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => (surj__ty_2Erealax_2Ereal(ap(ap(c_2Emeasure_2Einf__measure(A_27a),V0m),V1s)) = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Einf,ap(c_2Epred__set_2EGSPEC(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),f3510(A_27a,V1s,V0m))))))))))).
tff(ax_thm_2Emeasure_2Eclosed__cdi__def,axiom,( ! [A_27a:del]: ( ! [V0p:$i] : (mem(V0p,ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool))) => (p(ap(c_2Emeasure_2Eclosed__cdi(A_27a),V0p)) <=> (p(ap(ap(c_2Emeasure_2Esubset__class(A_27a),ap(c_2Emeasure_2Espace(A_27a),V0p)),ap(c_2Emeasure_2Esubsets(A_27a),V0p))) & (( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => (p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V1s),ap(c_2Emeasure_2Esubsets(A_27a),V0p))) => p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),ap(ap(c_2Epred__set_2EDIFF(A_27a),ap(c_2Emeasure_2Espace(A_27a),V0p)),V1s)),ap(c_2Emeasure_2Esubsets(A_27a),V0p)))))) & (( ! [V2f:$i] : (mem(V2f,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ((p(ap(ap(c_2Ebool_2EIN(arr(ty_2Enum_2Enum,arr(A_27a,bool))),V2f),ap(ap(c_2Epred__set_2EFUNSET(ty_2Enum_2Enum,arr(A_27a,bool)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),ap(c_2Emeasure_2Esubsets(A_27a),V0p)))) & ((ap(V2f,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)) = c_2Epred__set_2EEMPTY(A_27a)) & ( ! [V3n:tp__ty_2Enum_2Enum] : p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),ap(V2f,inj__ty_2Enum_2Enum(V3n))),ap(V2f,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V3n)))))))) => p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),ap(c_2Epred__set_2EBIGUNION(A_27a),ap(ap(c_2Epred__set_2EIMAGE(ty_2Enum_2Enum,arr(A_27a,bool)),V2f),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)))),ap(c_2Emeasure_2Esubsets(A_27a),V0p)))))) & ( ! [V4f:$i] : (mem(V4f,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ((p(ap(ap(c_2Ebool_2EIN(arr(ty_2Enum_2Enum,arr(A_27a,bool))),V4f),ap(ap(c_2Epred__set_2EFUNSET(ty_2Enum_2Enum,arr(A_27a,bool)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),ap(c_2Emeasure_2Esubsets(A_27a),V0p)))) & ( ! [V5m:tp__ty_2Enum_2Enum] : ( ! [V6n:tp__ty_2Enum_2Enum] : ((~~ (V5m = V6n)) => p(ap(ap(c_2Epred__set_2EDISJOINT(A_27a),ap(V4f,inj__ty_2Enum_2Enum(V5m))),ap(V4f,inj__ty_2Enum_2Enum(V6n)))))))) => p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),ap(c_2Epred__set_2EBIGUNION(A_27a),ap(ap(c_2Epred__set_2EIMAGE(ty_2Enum_2Enum,arr(A_27a,bool)),V4f),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)))),ap(c_2Emeasure_2Esubsets(A_27a),V0p)))))))))))))).
tff(ax_thm_2Emeasure_2Esmallest__closed__cdi__def,axiom,( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool))) => (ap(c_2Emeasure_2Esmallest__closed__cdi(A_27a),V0a) = ap(ap(c_2Epair_2E_2C(arr(A_27a,bool),arr(arr(A_27a,bool),bool)),ap(c_2Emeasure_2Espace(A_27a),V0a)),ap(c_2Epred__set_2EBIGINTER(arr(A_27a,bool)),ap(c_2Epred__set_2EGSPEC(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),bool)),f3511(A_27a,V0a))))))))).
tff(ax_thm_2Emeasure_2Emeasurable__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool))) => ( ! [V1b:$i] : (mem(V1b,ty_2Epair_2Eprod(arr(A_27b,bool),arr(arr(A_27b,bool),bool))) => (ap(ap(c_2Emeasure_2Emeasurable(A_27a,A_27b),V0a),V1b) = ap(c_2Epred__set_2EGSPEC(arr(A_27a,A_27b),arr(A_27a,A_27b)),f3513(A_27b,A_27a,V0a,V1b)))))))))).
tff(ax_thm_2Emeasure_2Emeasure__preserving__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0m1:$i] : (mem(V0m1,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1m2:$i] : (mem(V1m2,ty_2Epair_2Eprod(arr(A_27b,bool),ty_2Epair_2Eprod(arr(arr(A_27b,bool),bool),arr(arr(A_27b,bool),ty_2Erealax_2Ereal)))) => (ap(ap(c_2Emeasure_2Emeasure__preserving(A_27a,A_27b),V0m1),V1m2) = ap(c_2Epred__set_2EGSPEC(arr(A_27a,A_27b),arr(A_27a,A_27b)),f3515(A_27b,A_27a,V0m1,V1m2)))))))))).
tff(ax_thm_2Emeasure_2Eindicator__fn__def,axiom,( ! [A_27a:del]: ( ! [V0s:$i] : (mem(V0s,arr(A_27a,bool)) => (ap(c_2Emeasure_2Eindicator__fn(A_27a),V0s) = f3442(A_27a,V0s)))))).
tff(ax_thm_2Emeasure_2Epos__simple__fn__def,axiom,( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1f:$i] : (mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ! [V2s:$i] : (mem(V2s,arr(ty_2Enum_2Enum,bool)) => ( ! [V3a:$i] : (mem(V3a,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ( ! [V4x:$i] : (mem(V4x,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => (p(ap(ap(ap(ap(ap(c_2Emeasure_2Epos__simple__fn(A_27a),V0m),V1f),V2s),V3a),V4x)) <=> (( ! [V5t:$i] : (mem(V5t,A_27a) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(V1f,V5t))))) & (( ! [V6t:$i] : (mem(V6t,A_27a) => (p(ap(ap(c_2Ebool_2EIN(A_27a),V6t),ap(c_2Emeasure_2Em__space(A_27a),V0m))) => (surj__ty_2Eextreal_2Eextreal(ap(V1f,V6t)) = surj__ty_2Eextreal_2Eextreal(ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(ty_2Enum_2Enum),f3516(A_27a,V6t,V3a,V4x)),V2s)))))) & (( ! [V8i:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V8i)),V2s)) => p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),ap(V3a,inj__ty_2Enum_2Enum(V8i))),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m))))) & (p(ap(c_2Epred__set_2EFINITE(ty_2Enum_2Enum),V2s)) & (( ! [V9i:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V9i)),V2s)) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(V4x,inj__ty_2Enum_2Enum(V9i)))))) & (( ! [V10i:tp__ty_2Enum_2Enum] : ( ! [V11j:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V10i)),V2s)) & (p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V11j)),V2s)) & (~~ (V10i = V11j)))) => p(ap(ap(c_2Epred__set_2EDISJOINT(A_27a),ap(V3a,inj__ty_2Enum_2Enum(V10i))),ap(V3a,inj__ty_2Enum_2Enum(V11j))))))) & (ap(c_2Epred__set_2EBIGUNION(A_27a),ap(ap(c_2Epred__set_2EIMAGE(ty_2Enum_2Enum,arr(A_27a,bool)),V3a),V2s)) = ap(c_2Emeasure_2Em__space(A_27a),V0m))))))))))))))))))))).
tff(ax_thm_2Emeasure_2Enull__set__def,axiom,( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => (p(ap(ap(c_2Emeasure_2Enull__set(A_27a),V0m),V1s)) <=> (p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V1s),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m))) & (surj__ty_2Erealax_2Ereal(ap(ap(c_2Emeasure_2Emeasure(A_27a),V0m),V1s)) = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))))))).
tff(conj_thm_2Emeasure_2ESPACE,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool))) => (ap(ap(c_2Epair_2E_2C(arr(A_27a,bool),arr(arr(A_27a,bool),bool)),ap(c_2Emeasure_2Espace(A_27a),V0a)),ap(c_2Emeasure_2Esubsets(A_27a),V0a)) = V0a)))))).
tff(conj_thm_2Emeasure_2EALGEBRA__ALT__INTER,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool))) => (p(ap(c_2Emeasure_2Ealgebra(A_27a),V0a)) <=> (p(ap(ap(c_2Emeasure_2Esubset__class(A_27a),ap(c_2Emeasure_2Espace(A_27a),V0a)),ap(c_2Emeasure_2Esubsets(A_27a),V0a))) & (p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),c_2Epred__set_2EEMPTY(A_27a)),ap(c_2Emeasure_2Esubsets(A_27a),V0a))) & (( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => (p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V1s),ap(c_2Emeasure_2Esubsets(A_27a),V0a))) => p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),ap(ap(c_2Epred__set_2EDIFF(A_27a),ap(c_2Emeasure_2Espace(A_27a),V0a)),V1s)),ap(c_2Emeasure_2Esubsets(A_27a),V0a)))))) & ( ! [V2s:$i] : (mem(V2s,arr(A_27a,bool)) => ( ! [V3t:$i] : (mem(V3t,arr(A_27a,bool)) => ((p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V2s),ap(c_2Emeasure_2Esubsets(A_27a),V0a))) & p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V3t),ap(c_2Emeasure_2Esubsets(A_27a),V0a)))) => p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),ap(ap(c_2Epred__set_2EINTER(A_27a),V2s),V3t)),ap(c_2Emeasure_2Esubsets(A_27a),V0a))))))))))))))))).
tff(conj_thm_2Emeasure_2EALGEBRA__EMPTY,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool))) => (p(ap(c_2Emeasure_2Ealgebra(A_27a),V0a)) => p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),c_2Epred__set_2EEMPTY(A_27a)),ap(c_2Emeasure_2Esubsets(A_27a),V0a))))))))).
tff(conj_thm_2Emeasure_2EALGEBRA__SPACE,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool))) => (p(ap(c_2Emeasure_2Ealgebra(A_27a),V0a)) => p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),ap(c_2Emeasure_2Espace(A_27a),V0a)),ap(c_2Emeasure_2Esubsets(A_27a),V0a))))))))).
tff(conj_thm_2Emeasure_2EALGEBRA__COMPL,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool))) => ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => ((p(ap(c_2Emeasure_2Ealgebra(A_27a),V0a)) & p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V1s),ap(c_2Emeasure_2Esubsets(A_27a),V0a)))) => p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),ap(ap(c_2Epred__set_2EDIFF(A_27a),ap(c_2Emeasure_2Espace(A_27a),V0a)),V1s)),ap(c_2Emeasure_2Esubsets(A_27a),V0a))))))))))).
tff(conj_thm_2Emeasure_2EALGEBRA__UNION,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool))) => ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => ( ! [V2t:$i] : (mem(V2t,arr(A_27a,bool)) => ((p(ap(c_2Emeasure_2Ealgebra(A_27a),V0a)) & (p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V1s),ap(c_2Emeasure_2Esubsets(A_27a),V0a))) & p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V2t),ap(c_2Emeasure_2Esubsets(A_27a),V0a))))) => p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),ap(ap(c_2Epred__set_2EUNION(A_27a),V1s),V2t)),ap(c_2Emeasure_2Esubsets(A_27a),V0a))))))))))))).
tff(conj_thm_2Emeasure_2EALGEBRA__INTER,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool))) => ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => ( ! [V2t:$i] : (mem(V2t,arr(A_27a,bool)) => ((p(ap(c_2Emeasure_2Ealgebra(A_27a),V0a)) & (p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V1s),ap(c_2Emeasure_2Esubsets(A_27a),V0a))) & p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V2t),ap(c_2Emeasure_2Esubsets(A_27a),V0a))))) => p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),ap(ap(c_2Epred__set_2EINTER(A_27a),V1s),V2t)),ap(c_2Emeasure_2Esubsets(A_27a),V0a))))))))))))).
tff(conj_thm_2Emeasure_2EALGEBRA__DIFF,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool))) => ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => ( ! [V2t:$i] : (mem(V2t,arr(A_27a,bool)) => ((p(ap(c_2Emeasure_2Ealgebra(A_27a),V0a)) & (p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V1s),ap(c_2Emeasure_2Esubsets(A_27a),V0a))) & p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V2t),ap(c_2Emeasure_2Esubsets(A_27a),V0a))))) => p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),ap(ap(c_2Epred__set_2EDIFF(A_27a),V1s),V2t)),ap(c_2Emeasure_2Esubsets(A_27a),V0a))))))))))))).
tff(conj_thm_2Emeasure_2EALGEBRA__FINITE__UNION,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool))) => ( ! [V1c:$i] : (mem(V1c,arr(arr(A_27a,bool),bool)) => ((p(ap(c_2Emeasure_2Ealgebra(A_27a),V0a)) & (p(ap(c_2Epred__set_2EFINITE(arr(A_27a,bool)),V1c)) & p(ap(ap(c_2Epred__set_2ESUBSET(arr(A_27a,bool)),V1c),ap(c_2Emeasure_2Esubsets(A_27a),V0a))))) => p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),ap(c_2Epred__set_2EBIGUNION(A_27a),V1c)),ap(c_2Emeasure_2Esubsets(A_27a),V0a))))))))))).
tff(conj_thm_2Emeasure_2EALGEBRA__INTER__SPACE,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool))) => ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => ((p(ap(c_2Emeasure_2Ealgebra(A_27a),V0a)) & p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V1s),ap(c_2Emeasure_2Esubsets(A_27a),V0a)))) => ((ap(ap(c_2Epred__set_2EINTER(A_27a),ap(c_2Emeasure_2Espace(A_27a),V0a)),V1s) = V1s) & (ap(ap(c_2Epred__set_2EINTER(A_27a),V1s),ap(c_2Emeasure_2Espace(A_27a),V0a)) = V1s)))))))))).
tff(conj_thm_2Emeasure_2ELAMBDA__SYSTEM__EMPTY,lemma,(( ! [A_27a:del]: ( ! [V0g0:$i] : (mem(V0g0,ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool))) => ( ! [V1lam:$i] : (mem(V1lam,arr(arr(A_27a,bool),ty_2Erealax_2Ereal)) => ((p(ap(c_2Emeasure_2Ealgebra(A_27a),V0g0)) & p(ap(c_2Emeasure_2Epositive(A_27a),ap(ap(c_2Epair_2E_2C(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))),ap(c_2Emeasure_2Espace(A_27a),V0g0)),ap(ap(c_2Epair_2E_2C(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)),ap(c_2Emeasure_2Esubsets(A_27a),V0g0)),V1lam))))) => p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),c_2Epred__set_2EEMPTY(A_27a)),ap(ap(c_2Emeasure_2Elambda__system(A_27a),V0g0),V1lam))))))))))).
tff(conj_thm_2Emeasure_2ELAMBDA__SYSTEM__COMPL,lemma,(( ! [A_27a:del]: ( ! [V0g0:$i] : (mem(V0g0,ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool))) => ( ! [V1lam:$i] : (mem(V1lam,arr(arr(A_27a,bool),ty_2Erealax_2Ereal)) => ( ! [V2l:$i] : (mem(V2l,arr(A_27a,bool)) => ((p(ap(c_2Emeasure_2Ealgebra(A_27a),V0g0)) & (p(ap(c_2Emeasure_2Epositive(A_27a),ap(ap(c_2Epair_2E_2C(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))),ap(c_2Emeasure_2Espace(A_27a),V0g0)),ap(ap(c_2Epair_2E_2C(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)),ap(c_2Emeasure_2Esubsets(A_27a),V0g0)),V1lam)))) & p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V2l),ap(ap(c_2Emeasure_2Elambda__system(A_27a),V0g0),V1lam))))) => p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),ap(ap(c_2Epred__set_2EDIFF(A_27a),ap(c_2Emeasure_2Espace(A_27a),V0g0)),V2l)),ap(ap(c_2Emeasure_2Elambda__system(A_27a),V0g0),V1lam))))))))))))).
tff(conj_thm_2Emeasure_2ELAMBDA__SYSTEM__INTER,lemma,(( ! [A_27a:del]: ( ! [V0g0:$i] : (mem(V0g0,ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool))) => ( ! [V1lam:$i] : (mem(V1lam,arr(arr(A_27a,bool),ty_2Erealax_2Ereal)) => ( ! [V2l1:$i] : (mem(V2l1,arr(A_27a,bool)) => ( ! [V3l2:$i] : (mem(V3l2,arr(A_27a,bool)) => ((p(ap(c_2Emeasure_2Ealgebra(A_27a),V0g0)) & (p(ap(c_2Emeasure_2Epositive(A_27a),ap(ap(c_2Epair_2E_2C(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))),ap(c_2Emeasure_2Espace(A_27a),V0g0)),ap(ap(c_2Epair_2E_2C(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)),ap(c_2Emeasure_2Esubsets(A_27a),V0g0)),V1lam)))) & (p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V2l1),ap(ap(c_2Emeasure_2Elambda__system(A_27a),V0g0),V1lam))) & p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V3l2),ap(ap(c_2Emeasure_2Elambda__system(A_27a),V0g0),V1lam)))))) => p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),ap(ap(c_2Epred__set_2EINTER(A_27a),V2l1),V3l2)),ap(ap(c_2Emeasure_2Elambda__system(A_27a),V0g0),V1lam))))))))))))))).
tff(conj_thm_2Emeasure_2ELAMBDA__SYSTEM__ALGEBRA,lemma,(( ! [A_27a:del]: ( ! [V0g0:$i] : (mem(V0g0,ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool))) => ( ! [V1lam:$i] : (mem(V1lam,arr(arr(A_27a,bool),ty_2Erealax_2Ereal)) => ((p(ap(c_2Emeasure_2Ealgebra(A_27a),V0g0)) & p(ap(c_2Emeasure_2Epositive(A_27a),ap(ap(c_2Epair_2E_2C(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))),ap(c_2Emeasure_2Espace(A_27a),V0g0)),ap(ap(c_2Epair_2E_2C(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)),ap(c_2Emeasure_2Esubsets(A_27a),V0g0)),V1lam))))) => p(ap(c_2Emeasure_2Ealgebra(A_27a),ap(ap(c_2Epair_2E_2C(arr(A_27a,bool),arr(arr(A_27a,bool),bool)),ap(c_2Emeasure_2Espace(A_27a),V0g0)),ap(ap(c_2Emeasure_2Elambda__system(A_27a),V0g0),V1lam)))))))))))).
tff(conj_thm_2Emeasure_2ELAMBDA__SYSTEM__STRONG__ADDITIVE,lemma,(( ! [A_27a:del]: ( ! [V0g0:$i] : (mem(V0g0,ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool))) => ( ! [V1lam:$i] : (mem(V1lam,arr(arr(A_27a,bool),ty_2Erealax_2Ereal)) => ( ! [V2g:$i] : (mem(V2g,arr(A_27a,bool)) => ( ! [V3l1:$i] : (mem(V3l1,arr(A_27a,bool)) => ( ! [V4l2:$i] : (mem(V4l2,arr(A_27a,bool)) => ((p(ap(c_2Emeasure_2Ealgebra(A_27a),V0g0)) & (p(ap(c_2Emeasure_2Epositive(A_27a),ap(ap(c_2Epair_2E_2C(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))),ap(c_2Emeasure_2Espace(A_27a),V0g0)),ap(ap(c_2Epair_2E_2C(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)),ap(c_2Emeasure_2Esubsets(A_27a),V0g0)),V1lam)))) & (p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V2g),ap(c_2Emeasure_2Esubsets(A_27a),V0g0))) & (p(ap(ap(c_2Epred__set_2EDISJOINT(A_27a),V3l1),V4l2)) & (p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V3l1),ap(ap(c_2Emeasure_2Elambda__system(A_27a),V0g0),V1lam))) & p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V4l2),ap(ap(c_2Emeasure_2Elambda__system(A_27a),V0g0),V1lam)))))))) => (surj__ty_2Erealax_2Ereal(ap(V1lam,ap(ap(c_2Epred__set_2EINTER(A_27a),ap(ap(c_2Epred__set_2EUNION(A_27a),V3l1),V4l2)),V2g))) = surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__add,ap(V1lam,ap(ap(c_2Epred__set_2EINTER(A_27a),V3l1),V2g))),ap(V1lam,ap(ap(c_2Epred__set_2EINTER(A_27a),V4l2),V2g))))))))))))))))))).
tff(conj_thm_2Emeasure_2ELAMBDA__SYSTEM__ADDITIVE,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0g0:$i] : (mem(V0g0,ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool))) => ( ! [V1lam:$i] : (mem(V1lam,arr(arr(A_27a,bool),ty_2Erealax_2Ereal)) => ( ! [V2l1:$i] : (mem(V2l1,A_27b) => ( ! [V3l2:$i] : (mem(V3l2,A_27c) => ((p(ap(c_2Emeasure_2Ealgebra(A_27a),V0g0)) & p(ap(c_2Emeasure_2Epositive(A_27a),ap(ap(c_2Epair_2E_2C(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))),ap(c_2Emeasure_2Espace(A_27a),V0g0)),ap(ap(c_2Epair_2E_2C(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)),ap(c_2Emeasure_2Esubsets(A_27a),V0g0)),V1lam))))) => p(ap(c_2Emeasure_2Eadditive(A_27a),ap(ap(c_2Epair_2E_2C(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))),ap(c_2Emeasure_2Espace(A_27a),V0g0)),ap(ap(c_2Epair_2E_2C(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)),ap(ap(c_2Emeasure_2Elambda__system(A_27a),V0g0),V1lam)),V1lam)))))))))))))))))).
tff(conj_thm_2Emeasure_2ECOUNTABLY__SUBADDITIVE__SUBADDITIVE,lemma,(( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ((p(ap(c_2Emeasure_2Ealgebra(A_27a),ap(ap(c_2Epair_2E_2C(arr(A_27a,bool),arr(arr(A_27a,bool),bool)),ap(c_2Emeasure_2Em__space(A_27a),V0m)),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m)))) & (p(ap(c_2Emeasure_2Epositive(A_27a),V0m)) & p(ap(c_2Emeasure_2Ecountably__subadditive(A_27a),V0m)))) => p(ap(c_2Emeasure_2Esubadditive(A_27a),V0m)))))))).
tff(conj_thm_2Emeasure_2ESIGMA__ALGEBRA__ALT,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool))) => (p(ap(c_2Emeasure_2Esigma__algebra(A_27a),V0a)) <=> (p(ap(c_2Emeasure_2Ealgebra(A_27a),V0a)) & ( ! [V1f:$i] : (mem(V1f,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => (p(ap(ap(c_2Ebool_2EIN(arr(ty_2Enum_2Enum,arr(A_27a,bool))),V1f),ap(ap(c_2Epred__set_2EFUNSET(ty_2Enum_2Enum,arr(A_27a,bool)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),ap(c_2Emeasure_2Esubsets(A_27a),V0a)))) => p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),ap(c_2Epred__set_2EBIGUNION(A_27a),ap(ap(c_2Epred__set_2EIMAGE(ty_2Enum_2Enum,arr(A_27a,bool)),V1f),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)))),ap(c_2Emeasure_2Esubsets(A_27a),V0a))))))))))))).
tff(conj_thm_2Emeasure_2ESIGMA__ALGEBRA__ALT__MONO,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool))) => (p(ap(c_2Emeasure_2Esigma__algebra(A_27a),V0a)) <=> (p(ap(c_2Emeasure_2Ealgebra(A_27a),V0a)) & ( ! [V1f:$i] : (mem(V1f,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ((p(ap(ap(c_2Ebool_2EIN(arr(ty_2Enum_2Enum,arr(A_27a,bool))),V1f),ap(ap(c_2Epred__set_2EFUNSET(ty_2Enum_2Enum,arr(A_27a,bool)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),ap(c_2Emeasure_2Esubsets(A_27a),V0a)))) & ((ap(V1f,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)) = c_2Epred__set_2EEMPTY(A_27a)) & ( ! [V2n:tp__ty_2Enum_2Enum] : p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),ap(V1f,inj__ty_2Enum_2Enum(V2n))),ap(V1f,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V2n)))))))) => p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),ap(c_2Epred__set_2EBIGUNION(A_27a),ap(ap(c_2Epred__set_2EIMAGE(ty_2Enum_2Enum,arr(A_27a,bool)),V1f),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)))),ap(c_2Emeasure_2Esubsets(A_27a),V0a))))))))))))).
tff(conj_thm_2Emeasure_2ESIGMA__ALGEBRA__ALT__DISJOINT,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool))) => (p(ap(c_2Emeasure_2Esigma__algebra(A_27a),V0a)) <=> (p(ap(c_2Emeasure_2Ealgebra(A_27a),V0a)) & ( ! [V1f:$i] : (mem(V1f,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ((p(ap(ap(c_2Ebool_2EIN(arr(ty_2Enum_2Enum,arr(A_27a,bool))),V1f),ap(ap(c_2Epred__set_2EFUNSET(ty_2Enum_2Enum,arr(A_27a,bool)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),ap(c_2Emeasure_2Esubsets(A_27a),V0a)))) & ( ! [V2m:tp__ty_2Enum_2Enum] : ( ! [V3n:tp__ty_2Enum_2Enum] : ((~~ (V2m = V3n)) => p(ap(ap(c_2Epred__set_2EDISJOINT(A_27a),ap(V1f,inj__ty_2Enum_2Enum(V2m))),ap(V1f,inj__ty_2Enum_2Enum(V3n)))))))) => p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),ap(c_2Epred__set_2EBIGUNION(A_27a),ap(ap(c_2Epred__set_2EIMAGE(ty_2Enum_2Enum,arr(A_27a,bool)),V1f),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)))),ap(c_2Emeasure_2Esubsets(A_27a),V0a))))))))))))).
tff(conj_thm_2Emeasure_2ESUBADDITIVE,lemma,(( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => ( ! [V2t:$i] : (mem(V2t,arr(A_27a,bool)) => ( ! [V3u:$i] : (mem(V3u,arr(A_27a,bool)) => ((p(ap(c_2Emeasure_2Esubadditive(A_27a),V0m)) & (p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V1s),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m))) & (p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V2t),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m))) & (V3u = ap(ap(c_2Epred__set_2EUNION(A_27a),V1s),V2t))))) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Emeasure_2Emeasure(A_27a),V0m),V3u)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Emeasure_2Emeasure(A_27a),V0m),V1s)),ap(ap(c_2Emeasure_2Emeasure(A_27a),V0m),V2t)))))))))))))))).
tff(conj_thm_2Emeasure_2EADDITIVE,lemma,(( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => ( ! [V2t:$i] : (mem(V2t,arr(A_27a,bool)) => ( ! [V3u:$i] : (mem(V3u,arr(A_27a,bool)) => ((p(ap(c_2Emeasure_2Eadditive(A_27a),V0m)) & (p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V1s),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m))) & (p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V2t),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m))) & (p(ap(ap(c_2Epred__set_2EDISJOINT(A_27a),V1s),V2t)) & (V3u = ap(ap(c_2Epred__set_2EUNION(A_27a),V1s),V2t)))))) => (surj__ty_2Erealax_2Ereal(ap(ap(c_2Emeasure_2Emeasure(A_27a),V0m),V3u)) = surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Emeasure_2Emeasure(A_27a),V0m),V1s)),ap(ap(c_2Emeasure_2Emeasure(A_27a),V0m),V2t)))))))))))))))).
tff(conj_thm_2Emeasure_2ECOUNTABLY__SUBADDITIVE,lemma,(( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1f:$i] : (mem(V1f,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ( ! [V2s:$i] : (mem(V2s,arr(A_27a,bool)) => ((p(ap(c_2Emeasure_2Ecountably__subadditive(A_27a),V0m)) & (p(ap(ap(c_2Ebool_2EIN(arr(ty_2Enum_2Enum,arr(A_27a,bool))),V1f),ap(ap(c_2Epred__set_2EFUNSET(ty_2Enum_2Enum,arr(A_27a,bool)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m)))) & (p(ap(c_2Eseq_2Esummable,ap(ap(c_2Ecombin_2Eo(ty_2Enum_2Enum,ty_2Erealax_2Ereal,arr(A_27a,bool)),ap(c_2Emeasure_2Emeasure(A_27a),V0m)),V1f))) & ((V2s = ap(c_2Epred__set_2EBIGUNION(A_27a),ap(ap(c_2Epred__set_2EIMAGE(ty_2Enum_2Enum,arr(A_27a,bool)),V1f),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)))) & p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V2s),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m))))))) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Emeasure_2Emeasure(A_27a),V0m),V2s)),ap(c_2Eseq_2Esuminf,ap(ap(c_2Ecombin_2Eo(ty_2Enum_2Enum,ty_2Erealax_2Ereal,arr(A_27a,bool)),ap(c_2Emeasure_2Emeasure(A_27a),V0m)),V1f)))))))))))))).
tff(conj_thm_2Emeasure_2EADDITIVE__SUM,lemma,(( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1f:$i] : (mem(V1f,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ( ! [V2n:tp__ty_2Enum_2Enum] : ((p(ap(c_2Emeasure_2Ealgebra(A_27a),ap(ap(c_2Epair_2E_2C(arr(A_27a,bool),arr(arr(A_27a,bool),bool)),ap(c_2Emeasure_2Em__space(A_27a),V0m)),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m)))) & (p(ap(c_2Emeasure_2Epositive(A_27a),V0m)) & (p(ap(c_2Emeasure_2Eadditive(A_27a),V0m)) & (p(ap(ap(c_2Ebool_2EIN(arr(ty_2Enum_2Enum,arr(A_27a,bool))),V1f),ap(ap(c_2Epred__set_2EFUNSET(ty_2Enum_2Enum,arr(A_27a,bool)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m)))) & ( ! [V3m:tp__ty_2Enum_2Enum] : ( ! [V4n:tp__ty_2Enum_2Enum] : ((~~ (V3m = V4n)) => p(ap(ap(c_2Epred__set_2EDISJOINT(A_27a),ap(V1f,inj__ty_2Enum_2Enum(V3m))),ap(V1f,inj__ty_2Enum_2Enum(V4n))))))))))) => (surj__ty_2Erealax_2Ereal(ap(ap(c_2Ereal_2Esum,ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Enum_2Enum),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V2n))),ap(ap(c_2Ecombin_2Eo(ty_2Enum_2Enum,ty_2Erealax_2Ereal,arr(A_27a,bool)),ap(c_2Emeasure_2Emeasure(A_27a),V0m)),V1f))) = surj__ty_2Erealax_2Ereal(ap(ap(c_2Emeasure_2Emeasure(A_27a),V0m),ap(c_2Epred__set_2EBIGUNION(A_27a),ap(ap(c_2Epred__set_2EIMAGE(ty_2Enum_2Enum,arr(A_27a,bool)),V1f),ap(c_2Epred__set_2Ecount,inj__ty_2Enum_2Enum(V2n)))))))))))))))).
tff(conj_thm_2Emeasure_2EINCREASING__ADDITIVE__SUMMABLE,lemma,(( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1f:$i] : (mem(V1f,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ((p(ap(c_2Emeasure_2Ealgebra(A_27a),ap(ap(c_2Epair_2E_2C(arr(A_27a,bool),arr(arr(A_27a,bool),bool)),ap(c_2Emeasure_2Em__space(A_27a),V0m)),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m)))) & (p(ap(c_2Emeasure_2Epositive(A_27a),V0m)) & (p(ap(c_2Emeasure_2Eincreasing(A_27a),V0m)) & (p(ap(c_2Emeasure_2Eadditive(A_27a),V0m)) & (p(ap(ap(c_2Ebool_2EIN(arr(ty_2Enum_2Enum,arr(A_27a,bool))),V1f),ap(ap(c_2Epred__set_2EFUNSET(ty_2Enum_2Enum,arr(A_27a,bool)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m)))) & ( ! [V2m:tp__ty_2Enum_2Enum] : ( ! [V3n:tp__ty_2Enum_2Enum] : ((~~ (V2m = V3n)) => p(ap(ap(c_2Epred__set_2EDISJOINT(A_27a),ap(V1f,inj__ty_2Enum_2Enum(V2m))),ap(V1f,inj__ty_2Enum_2Enum(V3n)))))))))))) => p(ap(c_2Eseq_2Esummable,ap(ap(c_2Ecombin_2Eo(ty_2Enum_2Enum,ty_2Erealax_2Ereal,arr(A_27a,bool)),ap(c_2Emeasure_2Emeasure(A_27a),V0m)),V1f))))))))))).
tff(conj_thm_2Emeasure_2ELAMBDA__SYSTEM__POSITIVE,lemma,(( ! [A_27a:del]: ( ! [V0g0:$i] : (mem(V0g0,ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool))) => ( ! [V1lam:$i] : (mem(V1lam,arr(arr(A_27a,bool),ty_2Erealax_2Ereal)) => (p(ap(c_2Emeasure_2Epositive(A_27a),ap(ap(c_2Epair_2E_2C(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))),ap(c_2Emeasure_2Espace(A_27a),V0g0)),ap(ap(c_2Epair_2E_2C(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)),ap(c_2Emeasure_2Esubsets(A_27a),V0g0)),V1lam)))) => p(ap(c_2Emeasure_2Epositive(A_27a),ap(ap(c_2Epair_2E_2C(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))),ap(c_2Emeasure_2Espace(A_27a),V0g0)),ap(ap(c_2Epair_2E_2C(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)),ap(ap(c_2Emeasure_2Elambda__system(A_27a),V0g0),V1lam)),V1lam)))))))))))).
tff(conj_thm_2Emeasure_2ELAMBDA__SYSTEM__INCREASING,lemma,(( ! [A_27a:del]: ( ! [V0g0:$i] : (mem(V0g0,ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool))) => ( ! [V1lam:$i] : (mem(V1lam,arr(arr(A_27a,bool),ty_2Erealax_2Ereal)) => (p(ap(c_2Emeasure_2Eincreasing(A_27a),ap(ap(c_2Epair_2E_2C(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))),ap(c_2Emeasure_2Espace(A_27a),V0g0)),ap(ap(c_2Epair_2E_2C(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)),ap(c_2Emeasure_2Esubsets(A_27a),V0g0)),V1lam)))) => p(ap(c_2Emeasure_2Eincreasing(A_27a),ap(ap(c_2Epair_2E_2C(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))),ap(c_2Emeasure_2Espace(A_27a),V0g0)),ap(ap(c_2Epair_2E_2C(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)),ap(ap(c_2Emeasure_2Elambda__system(A_27a),V0g0),V1lam)),V1lam)))))))))))).
tff(conj_thm_2Emeasure_2ELAMBDA__SYSTEM__STRONG__SUM,lemma,(( ! [A_27a:del]: ( ! [V0g0:$i] : (mem(V0g0,ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool))) => ( ! [V1lam:$i] : (mem(V1lam,arr(arr(A_27a,bool),ty_2Erealax_2Ereal)) => ( ! [V2g:$i] : (mem(V2g,arr(A_27a,bool)) => ( ! [V3f:$i] : (mem(V3f,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ( ! [V4n:tp__ty_2Enum_2Enum] : ((p(ap(c_2Emeasure_2Ealgebra(A_27a),V0g0)) & (p(ap(c_2Emeasure_2Epositive(A_27a),ap(ap(c_2Epair_2E_2C(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))),ap(c_2Emeasure_2Espace(A_27a),V0g0)),ap(ap(c_2Epair_2E_2C(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)),ap(c_2Emeasure_2Esubsets(A_27a),V0g0)),V1lam)))) & (p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V2g),ap(c_2Emeasure_2Esubsets(A_27a),V0g0))) & (p(ap(ap(c_2Ebool_2EIN(arr(ty_2Enum_2Enum,arr(A_27a,bool))),V3f),ap(ap(c_2Epred__set_2EFUNSET(ty_2Enum_2Enum,arr(A_27a,bool)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),ap(ap(c_2Emeasure_2Elambda__system(A_27a),V0g0),V1lam)))) & ( ! [V5m:tp__ty_2Enum_2Enum] : ( ! [V6n:tp__ty_2Enum_2Enum] : ((~~ (V5m = V6n)) => p(ap(ap(c_2Epred__set_2EDISJOINT(A_27a),ap(V3f,inj__ty_2Enum_2Enum(V5m))),ap(V3f,inj__ty_2Enum_2Enum(V6n))))))))))) => (surj__ty_2Erealax_2Ereal(ap(ap(c_2Ereal_2Esum,ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Enum_2Enum),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V4n))),ap(ap(c_2Ecombin_2Eo(ty_2Enum_2Enum,ty_2Erealax_2Ereal,arr(A_27a,bool)),V1lam),ap(ap(c_2Ecombin_2Eo(ty_2Enum_2Enum,arr(A_27a,bool),arr(A_27a,bool)),f3517(A_27a,V2g)),V3f)))) = surj__ty_2Erealax_2Ereal(ap(V1lam,ap(ap(c_2Epred__set_2EINTER(A_27a),ap(c_2Epred__set_2EBIGUNION(A_27a),ap(ap(c_2Epred__set_2EIMAGE(ty_2Enum_2Enum,arr(A_27a,bool)),V3f),ap(c_2Epred__set_2Ecount,inj__ty_2Enum_2Enum(V4n))))),V2g))))))))))))))))).
tff(conj_thm_2Emeasure_2ESIGMA__ALGEBRA__ALGEBRA,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool))) => (p(ap(c_2Emeasure_2Esigma__algebra(A_27a),V0a)) => p(ap(c_2Emeasure_2Ealgebra(A_27a),V0a)))))))).
tff(conj_thm_2Emeasure_2EOUTER__MEASURE__SPACE__POSITIVE,lemma,(( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => (p(ap(c_2Emeasure_2Eouter__measure__space(A_27a),V0m)) => p(ap(c_2Emeasure_2Epositive(A_27a),V0m)))))))).
tff(conj_thm_2Emeasure_2ELAMBDA__SYSTEM__CARATHEODORY,lemma,(( ! [A_27a:del]: ( ! [V0gsig:$i] : (mem(V0gsig,ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool))) => ( ! [V1lam:$i] : (mem(V1lam,arr(arr(A_27a,bool),ty_2Erealax_2Ereal)) => ((p(ap(c_2Emeasure_2Esigma__algebra(A_27a),V0gsig)) & p(ap(c_2Emeasure_2Eouter__measure__space(A_27a),ap(ap(c_2Epair_2E_2C(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))),ap(c_2Emeasure_2Espace(A_27a),V0gsig)),ap(ap(c_2Epair_2E_2C(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)),ap(c_2Emeasure_2Esubsets(A_27a),V0gsig)),V1lam))))) => ( ! [V2f:$i] : (mem(V2f,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ((p(ap(ap(c_2Ebool_2EIN(arr(ty_2Enum_2Enum,arr(A_27a,bool))),V2f),ap(ap(c_2Epred__set_2EFUNSET(ty_2Enum_2Enum,arr(A_27a,bool)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),ap(ap(c_2Emeasure_2Elambda__system(A_27a),V0gsig),V1lam)))) & ( ! [V3m:tp__ty_2Enum_2Enum] : ( ! [V4n:tp__ty_2Enum_2Enum] : ((~~ (V3m = V4n)) => p(ap(ap(c_2Epred__set_2EDISJOINT(A_27a),ap(V2f,inj__ty_2Enum_2Enum(V3m))),ap(V2f,inj__ty_2Enum_2Enum(V4n)))))))) => (p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),ap(c_2Epred__set_2EBIGUNION(A_27a),ap(ap(c_2Epred__set_2EIMAGE(ty_2Enum_2Enum,arr(A_27a,bool)),V2f),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)))),ap(ap(c_2Emeasure_2Elambda__system(A_27a),V0gsig),V1lam))) & p(ap(ap(c_2Eseq_2Esums,ap(ap(c_2Ecombin_2Eo(ty_2Enum_2Enum,ty_2Erealax_2Ereal,arr(A_27a,bool)),V1lam),V2f)),ap(V1lam,ap(c_2Epred__set_2EBIGUNION(A_27a),ap(ap(c_2Epred__set_2EIMAGE(ty_2Enum_2Enum,arr(A_27a,bool)),V2f),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)))))))))))))))))).
tff(conj_thm_2Emeasure_2ECARATHEODORY__LEMMA,lemma,(( ! [A_27a:del]: ( ! [V0gsig:$i] : (mem(V0gsig,ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool))) => ( ! [V1lam:$i] : (mem(V1lam,arr(arr(A_27a,bool),ty_2Erealax_2Ereal)) => ((p(ap(c_2Emeasure_2Esigma__algebra(A_27a),V0gsig)) & p(ap(c_2Emeasure_2Eouter__measure__space(A_27a),ap(ap(c_2Epair_2E_2C(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))),ap(c_2Emeasure_2Espace(A_27a),V0gsig)),ap(ap(c_2Epair_2E_2C(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)),ap(c_2Emeasure_2Esubsets(A_27a),V0gsig)),V1lam))))) => p(ap(c_2Emeasure_2Emeasure__space(A_27a),ap(ap(c_2Epair_2E_2C(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))),ap(c_2Emeasure_2Espace(A_27a),V0gsig)),ap(ap(c_2Epair_2E_2C(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)),ap(ap(c_2Emeasure_2Elambda__system(A_27a),V0gsig),V1lam)),V1lam)))))))))))).
tff(conj_thm_2Emeasure_2EINF__MEASURE__NONEMPTY,lemma,(( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1g:$i] : (mem(V1g,arr(A_27a,bool)) => ( ! [V2s:$i] : (mem(V2s,arr(A_27a,bool)) => ((p(ap(c_2Emeasure_2Ealgebra(A_27a),ap(ap(c_2Epair_2E_2C(arr(A_27a,bool),arr(arr(A_27a,bool),bool)),ap(c_2Emeasure_2Em__space(A_27a),V0m)),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m)))) & (p(ap(c_2Emeasure_2Epositive(A_27a),V0m)) & (p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V2s),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m))) & p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),V1g),V2s))))) => p(ap(ap(c_2Ebool_2EIN(ty_2Erealax_2Ereal),ap(ap(c_2Emeasure_2Emeasure(A_27a),V0m),V2s)),ap(c_2Epred__set_2EGSPEC(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),f3521(A_27a,V1g,V0m)))))))))))))).
tff(conj_thm_2Emeasure_2EINF__MEASURE__POS0,lemma,(( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1g:$i] : (mem(V1g,arr(A_27a,bool)) => ( ! [V2x:tp__ty_2Erealax_2Ereal] : ((p(ap(c_2Emeasure_2Ealgebra(A_27a),ap(ap(c_2Epair_2E_2C(arr(A_27a,bool),arr(arr(A_27a,bool),bool)),ap(c_2Emeasure_2Em__space(A_27a),V0m)),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m)))) & (p(ap(c_2Emeasure_2Epositive(A_27a),V0m)) & p(ap(ap(c_2Ebool_2EIN(ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V2x)),ap(c_2Epred__set_2EGSPEC(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),f3521(A_27a,V1g,V0m)))))) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Erealax_2Ereal(V2x)))))))))))).
tff(conj_thm_2Emeasure_2EINF__MEASURE__POS,lemma,(( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1g:$i] : (mem(V1g,arr(A_27a,bool)) => ((p(ap(c_2Emeasure_2Ealgebra(A_27a),ap(ap(c_2Epair_2E_2C(arr(A_27a,bool),arr(arr(A_27a,bool),bool)),ap(c_2Emeasure_2Em__space(A_27a),V0m)),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m)))) & (p(ap(c_2Emeasure_2Epositive(A_27a),V0m)) & p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),V1g),ap(c_2Emeasure_2Em__space(A_27a),V0m))))) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(ap(c_2Emeasure_2Einf__measure(A_27a),V0m),V1g))))))))))).
tff(conj_thm_2Emeasure_2EINCREASING,lemma,(( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => ( ! [V2t:$i] : (mem(V2t,arr(A_27a,bool)) => ((p(ap(c_2Emeasure_2Eincreasing(A_27a),V0m)) & (p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),V1s),V2t)) & (p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V1s),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m))) & p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V2t),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m)))))) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Emeasure_2Emeasure(A_27a),V0m),V1s)),ap(ap(c_2Emeasure_2Emeasure(A_27a),V0m),V2t))))))))))))).
tff(conj_thm_2Emeasure_2EADDITIVE__INCREASING,lemma,(( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ((p(ap(c_2Emeasure_2Ealgebra(A_27a),ap(ap(c_2Epair_2E_2C(arr(A_27a,bool),arr(arr(A_27a,bool),bool)),ap(c_2Emeasure_2Em__space(A_27a),V0m)),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m)))) & (p(ap(c_2Emeasure_2Epositive(A_27a),V0m)) & p(ap(c_2Emeasure_2Eadditive(A_27a),V0m)))) => p(ap(c_2Emeasure_2Eincreasing(A_27a),V0m)))))))).
tff(conj_thm_2Emeasure_2ECOUNTABLY__ADDITIVE__ADDITIVE,lemma,(( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ((p(ap(c_2Emeasure_2Ealgebra(A_27a),ap(ap(c_2Epair_2E_2C(arr(A_27a,bool),arr(arr(A_27a,bool),bool)),ap(c_2Emeasure_2Em__space(A_27a),V0m)),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m)))) & (p(ap(c_2Emeasure_2Epositive(A_27a),V0m)) & p(ap(c_2Emeasure_2Ecountably__additive(A_27a),V0m)))) => p(ap(c_2Emeasure_2Eadditive(A_27a),V0m)))))))).
tff(conj_thm_2Emeasure_2ECOUNTABLY__ADDITIVE,lemma,(( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => ( ! [V2f:$i] : (mem(V2f,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ((p(ap(c_2Emeasure_2Ecountably__additive(A_27a),V0m)) & (p(ap(ap(c_2Ebool_2EIN(arr(ty_2Enum_2Enum,arr(A_27a,bool))),V2f),ap(ap(c_2Epred__set_2EFUNSET(ty_2Enum_2Enum,arr(A_27a,bool)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m)))) & (( ! [V3m:tp__ty_2Enum_2Enum] : ( ! [V4n:tp__ty_2Enum_2Enum] : ((~~ (V3m = V4n)) => p(ap(ap(c_2Epred__set_2EDISJOINT(A_27a),ap(V2f,inj__ty_2Enum_2Enum(V3m))),ap(V2f,inj__ty_2Enum_2Enum(V4n))))))) & ((V1s = ap(c_2Epred__set_2EBIGUNION(A_27a),ap(ap(c_2Epred__set_2EIMAGE(ty_2Enum_2Enum,arr(A_27a,bool)),V2f),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)))) & p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V1s),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m))))))) => p(ap(ap(c_2Eseq_2Esums,ap(ap(c_2Ecombin_2Eo(ty_2Enum_2Enum,ty_2Erealax_2Ereal,arr(A_27a,bool)),ap(c_2Emeasure_2Emeasure(A_27a),V0m)),V2f)),ap(ap(c_2Emeasure_2Emeasure(A_27a),V0m),V1s))))))))))))).
tff(conj_thm_2Emeasure_2EINF__MEASURE__AGREES,lemma,(( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => ((p(ap(c_2Emeasure_2Ealgebra(A_27a),ap(ap(c_2Epair_2E_2C(arr(A_27a,bool),arr(arr(A_27a,bool),bool)),ap(c_2Emeasure_2Em__space(A_27a),V0m)),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m)))) & (p(ap(c_2Emeasure_2Epositive(A_27a),V0m)) & (p(ap(c_2Emeasure_2Ecountably__additive(A_27a),V0m)) & p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V1s),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m)))))) => (surj__ty_2Erealax_2Ereal(ap(ap(c_2Emeasure_2Einf__measure(A_27a),V0m),V1s)) = surj__ty_2Erealax_2Ereal(ap(ap(c_2Emeasure_2Emeasure(A_27a),V0m),V1s))))))))))).
tff(conj_thm_2Emeasure_2EMEASURE__DOWN,lemma,(( ! [A_27a:del]: ( ! [V0m0:$i] : (mem(V0m0,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1m1:$i] : (mem(V1m1,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ((p(ap(c_2Emeasure_2Esigma__algebra(A_27a),ap(ap(c_2Epair_2E_2C(arr(A_27a,bool),arr(arr(A_27a,bool),bool)),ap(c_2Emeasure_2Em__space(A_27a),V0m0)),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m0)))) & (p(ap(ap(c_2Epred__set_2ESUBSET(arr(A_27a,bool)),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m0)),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V1m1))) & ((ap(c_2Emeasure_2Emeasure(A_27a),V0m0) = ap(c_2Emeasure_2Emeasure(A_27a),V1m1)) & p(ap(c_2Emeasure_2Emeasure__space(A_27a),V1m1))))) => p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m0)))))))))).
tff(conj_thm_2Emeasure_2ESIGMA__ALGEBRA__SIGMA,lemma,(( ! [A_27a:del]: ( ! [V0sp:$i] : (mem(V0sp,arr(A_27a,bool)) => ( ! [V1sts:$i] : (mem(V1sts,arr(arr(A_27a,bool),bool)) => (p(ap(ap(c_2Emeasure_2Esubset__class(A_27a),V0sp),V1sts)) => p(ap(c_2Emeasure_2Esigma__algebra(A_27a),ap(ap(c_2Emeasure_2Esigma(A_27a),V0sp),V1sts))))))))))).
tff(conj_thm_2Emeasure_2EPOW__ALGEBRA,lemma,(( ! [A_27a:del]: ( ! [V0sp:$i] : (mem(V0sp,arr(A_27a,bool)) => p(ap(c_2Emeasure_2Ealgebra(A_27a),ap(ap(c_2Epair_2E_2C(arr(A_27a,bool),arr(arr(A_27a,bool),bool)),V0sp),ap(c_2Epred__set_2EPOW(A_27a),V0sp))))))))).
tff(conj_thm_2Emeasure_2EPOW__SIGMA__ALGEBRA,lemma,(( ! [A_27a:del]: ( ! [V0sp:$i] : (mem(V0sp,arr(A_27a,bool)) => p(ap(c_2Emeasure_2Esigma__algebra(A_27a),ap(ap(c_2Epair_2E_2C(arr(A_27a,bool),arr(arr(A_27a,bool),bool)),V0sp),ap(c_2Epred__set_2EPOW(A_27a),V0sp))))))))).
tff(conj_thm_2Emeasure_2EUNIV__SIGMA__ALGEBRA,lemma,(( ! [A_27a:del]: p(ap(c_2Emeasure_2Esigma__algebra(A_27a),ap(ap(c_2Epair_2E_2C(arr(A_27a,bool),arr(arr(A_27a,bool),bool)),c_2Epred__set_2EUNIV(A_27a)),c_2Epred__set_2EUNIV(arr(A_27a,bool)))))))).
tff(conj_thm_2Emeasure_2EINF__MEASURE__EMPTY,lemma,(( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ((p(ap(c_2Emeasure_2Ealgebra(A_27a),ap(ap(c_2Epair_2E_2C(arr(A_27a,bool),arr(arr(A_27a,bool),bool)),ap(c_2Emeasure_2Em__space(A_27a),V0m)),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m)))) & p(ap(c_2Emeasure_2Epositive(A_27a),V0m))) => (surj__ty_2Erealax_2Ereal(ap(ap(c_2Emeasure_2Einf__measure(A_27a),V0m),c_2Epred__set_2EEMPTY(A_27a))) = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))))).
tff(conj_thm_2Emeasure_2EINF__MEASURE__POSITIVE,lemma,(( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ((p(ap(c_2Emeasure_2Ealgebra(A_27a),ap(ap(c_2Epair_2E_2C(arr(A_27a,bool),arr(arr(A_27a,bool),bool)),ap(c_2Emeasure_2Em__space(A_27a),V0m)),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m)))) & p(ap(c_2Emeasure_2Epositive(A_27a),V0m))) => p(ap(c_2Emeasure_2Epositive(A_27a),ap(ap(c_2Epair_2E_2C(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))),ap(c_2Emeasure_2Em__space(A_27a),V0m)),ap(ap(c_2Epair_2E_2C(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)),ap(c_2Epred__set_2EPOW(A_27a),ap(c_2Emeasure_2Em__space(A_27a),V0m))),ap(c_2Emeasure_2Einf__measure(A_27a),V0m))))))))))).
tff(conj_thm_2Emeasure_2EINF__MEASURE__INCREASING,lemma,(( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ((p(ap(c_2Emeasure_2Ealgebra(A_27a),ap(ap(c_2Epair_2E_2C(arr(A_27a,bool),arr(arr(A_27a,bool),bool)),ap(c_2Emeasure_2Em__space(A_27a),V0m)),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m)))) & p(ap(c_2Emeasure_2Epositive(A_27a),V0m))) => p(ap(c_2Emeasure_2Eincreasing(A_27a),ap(ap(c_2Epair_2E_2C(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))),ap(c_2Emeasure_2Em__space(A_27a),V0m)),ap(ap(c_2Epair_2E_2C(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)),ap(c_2Epred__set_2EPOW(A_27a),ap(c_2Emeasure_2Em__space(A_27a),V0m))),ap(c_2Emeasure_2Einf__measure(A_27a),V0m))))))))))).
tff(conj_thm_2Emeasure_2EINF__MEASURE__LE,lemma,(( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => ( ! [V2x:tp__ty_2Erealax_2Ereal] : ((p(ap(c_2Emeasure_2Ealgebra(A_27a),ap(ap(c_2Epair_2E_2C(arr(A_27a,bool),arr(arr(A_27a,bool),bool)),ap(c_2Emeasure_2Em__space(A_27a),V0m)),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m)))) & (p(ap(c_2Emeasure_2Epositive(A_27a),V0m)) & (p(ap(c_2Emeasure_2Eincreasing(A_27a),V0m)) & p(ap(ap(c_2Ebool_2EIN(ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V2x)),ap(c_2Epred__set_2EGSPEC(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),f3523(A_27a,V1s,V0m))))))) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Emeasure_2Einf__measure(A_27a),V0m),V1s)),inj__ty_2Erealax_2Ereal(V2x)))))))))))).
tff(conj_thm_2Emeasure_2EINF__MEASURE__CLOSE,lemma,(( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => ( ! [V2e:tp__ty_2Erealax_2Ereal] : ((p(ap(c_2Emeasure_2Ealgebra(A_27a),ap(ap(c_2Epair_2E_2C(arr(A_27a,bool),arr(arr(A_27a,bool),bool)),ap(c_2Emeasure_2Em__space(A_27a),V0m)),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m)))) & (p(ap(c_2Emeasure_2Epositive(A_27a),V0m)) & (p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Erealax_2Ereal(V2e))) & p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),V1s),ap(c_2Emeasure_2Em__space(A_27a),V0m)))))) => (? [V3f:$i] : (mem(V3f,arr(ty_2Enum_2Enum,arr(A_27a,bool))) & (? [V4l:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Ebool_2EIN(arr(ty_2Enum_2Enum,arr(A_27a,bool))),V3f),ap(ap(c_2Epred__set_2EFUNSET(ty_2Enum_2Enum,arr(A_27a,bool)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m)))) & (p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),V1s),ap(c_2Epred__set_2EBIGUNION(A_27a),ap(ap(c_2Epred__set_2EIMAGE(ty_2Enum_2Enum,arr(A_27a,bool)),V3f),c_2Epred__set_2EUNIV(ty_2Enum_2Enum))))) & (( ! [V5m:tp__ty_2Enum_2Enum] : ( ! [V6n:tp__ty_2Enum_2Enum] : ((~~ (V5m = V6n)) => p(ap(ap(c_2Epred__set_2EDISJOINT(A_27a),ap(V3f,inj__ty_2Enum_2Enum(V5m))),ap(V3f,inj__ty_2Enum_2Enum(V6n))))))) & (p(ap(ap(c_2Eseq_2Esums,ap(ap(c_2Ecombin_2Eo(ty_2Enum_2Enum,ty_2Erealax_2Ereal,arr(A_27a,bool)),ap(c_2Emeasure_2Emeasure(A_27a),V0m)),V3f)),inj__ty_2Erealax_2Ereal(V4l))) & p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V4l)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Emeasure_2Einf__measure(A_27a),V0m),V1s)),inj__ty_2Erealax_2Ereal(V2e)))))))))))))))))))).
tff(conj_thm_2Emeasure_2EINF__MEASURE__COUNTABLY__SUBADDITIVE,lemma,(( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ((p(ap(c_2Emeasure_2Ealgebra(A_27a),ap(ap(c_2Epair_2E_2C(arr(A_27a,bool),arr(arr(A_27a,bool),bool)),ap(c_2Emeasure_2Em__space(A_27a),V0m)),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m)))) & (p(ap(c_2Emeasure_2Epositive(A_27a),V0m)) & p(ap(c_2Emeasure_2Eincreasing(A_27a),V0m)))) => p(ap(c_2Emeasure_2Ecountably__subadditive(A_27a),ap(ap(c_2Epair_2E_2C(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))),ap(c_2Emeasure_2Em__space(A_27a),V0m)),ap(ap(c_2Epair_2E_2C(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)),ap(c_2Epred__set_2EPOW(A_27a),ap(c_2Emeasure_2Em__space(A_27a),V0m))),ap(c_2Emeasure_2Einf__measure(A_27a),V0m))))))))))).
tff(conj_thm_2Emeasure_2EINF__MEASURE__OUTER,lemma,(( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ((p(ap(c_2Emeasure_2Ealgebra(A_27a),ap(ap(c_2Epair_2E_2C(arr(A_27a,bool),arr(arr(A_27a,bool),bool)),ap(c_2Emeasure_2Em__space(A_27a),V0m)),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m)))) & (p(ap(c_2Emeasure_2Epositive(A_27a),V0m)) & p(ap(c_2Emeasure_2Eincreasing(A_27a),V0m)))) => p(ap(c_2Emeasure_2Eouter__measure__space(A_27a),ap(ap(c_2Epair_2E_2C(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal))),ap(c_2Emeasure_2Em__space(A_27a),V0m)),ap(ap(c_2Epair_2E_2C(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)),ap(c_2Epred__set_2EPOW(A_27a),ap(c_2Emeasure_2Em__space(A_27a),V0m))),ap(c_2Emeasure_2Einf__measure(A_27a),V0m))))))))))).
tff(conj_thm_2Emeasure_2ESIGMA__SUBSET,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,arr(arr(A_27a,bool),bool)) => ( ! [V1b:$i] : (mem(V1b,ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool))) => ((p(ap(c_2Emeasure_2Esigma__algebra(A_27a),V1b)) & p(ap(ap(c_2Epred__set_2ESUBSET(arr(A_27a,bool)),V0a),ap(c_2Emeasure_2Esubsets(A_27a),V1b)))) => p(ap(ap(c_2Epred__set_2ESUBSET(arr(A_27a,bool)),ap(c_2Emeasure_2Esubsets(A_27a),ap(ap(c_2Emeasure_2Esigma(A_27a),ap(c_2Emeasure_2Espace(A_27a),V1b)),V0a))),ap(c_2Emeasure_2Esubsets(A_27a),V1b))))))))))).
tff(conj_thm_2Emeasure_2EALGEBRA__SUBSET__LAMBDA__SYSTEM,lemma,(( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ((p(ap(c_2Emeasure_2Ealgebra(A_27a),ap(ap(c_2Epair_2E_2C(arr(A_27a,bool),arr(arr(A_27a,bool),bool)),ap(c_2Emeasure_2Em__space(A_27a),V0m)),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m)))) & (p(ap(c_2Emeasure_2Epositive(A_27a),V0m)) & (p(ap(c_2Emeasure_2Eincreasing(A_27a),V0m)) & p(ap(c_2Emeasure_2Eadditive(A_27a),V0m))))) => p(ap(ap(c_2Epred__set_2ESUBSET(arr(A_27a,bool)),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m)),ap(ap(c_2Emeasure_2Elambda__system(A_27a),ap(ap(c_2Epair_2E_2C(arr(A_27a,bool),arr(arr(A_27a,bool),bool)),ap(c_2Emeasure_2Em__space(A_27a),V0m)),ap(c_2Epred__set_2EPOW(A_27a),ap(c_2Emeasure_2Em__space(A_27a),V0m)))),ap(c_2Emeasure_2Einf__measure(A_27a),V0m)))))))))).
tff(conj_thm_2Emeasure_2ECARATHEODORY,lemma,(( ! [A_27a:del]: ( ! [V0m0:$i] : (mem(V0m0,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ((p(ap(c_2Emeasure_2Ealgebra(A_27a),ap(ap(c_2Epair_2E_2C(arr(A_27a,bool),arr(arr(A_27a,bool),bool)),ap(c_2Emeasure_2Em__space(A_27a),V0m0)),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m0)))) & (p(ap(c_2Emeasure_2Epositive(A_27a),V0m0)) & p(ap(c_2Emeasure_2Ecountably__additive(A_27a),V0m0)))) => (? [V1m:$i] : (mem(V1m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) & (( ! [V2s:$i] : (mem(V2s,arr(A_27a,bool)) => (p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V2s),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m0))) => (surj__ty_2Erealax_2Ereal(ap(ap(c_2Emeasure_2Emeasure(A_27a),V1m),V2s)) = surj__ty_2Erealax_2Ereal(ap(ap(c_2Emeasure_2Emeasure(A_27a),V0m0),V2s)))))) & ((ap(ap(c_2Epair_2E_2C(arr(A_27a,bool),arr(arr(A_27a,bool),bool)),ap(c_2Emeasure_2Em__space(A_27a),V1m)),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V1m)) = ap(ap(c_2Emeasure_2Esigma(A_27a),ap(c_2Emeasure_2Em__space(A_27a),V0m0)),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m0))) & p(ap(c_2Emeasure_2Emeasure__space(A_27a),V1m)))))))))))).
tff(conj_thm_2Emeasure_2ESIGMA__SUBSET__SUBSETS,lemma,(( ! [A_27a:del]: ( ! [V0sp:$i] : (mem(V0sp,arr(A_27a,bool)) => ( ! [V1a:$i] : (mem(V1a,arr(arr(A_27a,bool),bool)) => p(ap(ap(c_2Epred__set_2ESUBSET(arr(A_27a,bool)),V1a),ap(c_2Emeasure_2Esubsets(A_27a),ap(ap(c_2Emeasure_2Esigma(A_27a),V0sp),V1a))))))))))).
tff(conj_thm_2Emeasure_2EIN__SIGMA,lemma,(( ! [A_27a:del]: ( ! [V0sp:$i] : (mem(V0sp,arr(A_27a,bool)) => ( ! [V1a:$i] : (mem(V1a,arr(arr(A_27a,bool),bool)) => ( ! [V2x:$i] : (mem(V2x,arr(A_27a,bool)) => (p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V2x),V1a)) => p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V2x),ap(c_2Emeasure_2Esubsets(A_27a),ap(ap(c_2Emeasure_2Esigma(A_27a),V0sp),V1a)))))))))))))).
tff(conj_thm_2Emeasure_2ESIGMA__ALGEBRA,lemma,(( ! [A_27a:del]: ( ! [V0p:$i] : (mem(V0p,ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool))) => (p(ap(c_2Emeasure_2Esigma__algebra(A_27a),V0p)) <=> (p(ap(ap(c_2Emeasure_2Esubset__class(A_27a),ap(c_2Emeasure_2Espace(A_27a),V0p)),ap(c_2Emeasure_2Esubsets(A_27a),V0p))) & (p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),c_2Epred__set_2EEMPTY(A_27a)),ap(c_2Emeasure_2Esubsets(A_27a),V0p))) & (( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => (p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V1s),ap(c_2Emeasure_2Esubsets(A_27a),V0p))) => p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),ap(ap(c_2Epred__set_2EDIFF(A_27a),ap(c_2Emeasure_2Espace(A_27a),V0p)),V1s)),ap(c_2Emeasure_2Esubsets(A_27a),V0p)))))) & ( ! [V2c:$i] : (mem(V2c,arr(arr(A_27a,bool),bool)) => ((p(ap(c_2Epred__set_2Ecountable(arr(A_27a,bool)),V2c)) & p(ap(ap(c_2Epred__set_2ESUBSET(arr(A_27a,bool)),V2c),ap(c_2Emeasure_2Esubsets(A_27a),V0p)))) => p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),ap(c_2Epred__set_2EBIGUNION(A_27a),V2c)),ap(c_2Emeasure_2Esubsets(A_27a),V0p))))))))))))))).
tff(conj_thm_2Emeasure_2ESIGMA__ALGEBRA__COUNTABLE__UNION,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool))) => ( ! [V1c:$i] : (mem(V1c,arr(arr(A_27a,bool),bool)) => ((p(ap(c_2Emeasure_2Esigma__algebra(A_27a),V0a)) & (p(ap(c_2Epred__set_2Ecountable(arr(A_27a,bool)),V1c)) & p(ap(ap(c_2Epred__set_2ESUBSET(arr(A_27a,bool)),V1c),ap(c_2Emeasure_2Esubsets(A_27a),V0a))))) => p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),ap(c_2Epred__set_2EBIGUNION(A_27a),V1c)),ap(c_2Emeasure_2Esubsets(A_27a),V0a))))))))))).
tff(conj_thm_2Emeasure_2ESIGMA__ALGEBRA__ENUM,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool))) => ( ! [V1f:$i] : (mem(V1f,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ((p(ap(c_2Emeasure_2Esigma__algebra(A_27a),V0a)) & p(ap(ap(c_2Ebool_2EIN(arr(ty_2Enum_2Enum,arr(A_27a,bool))),V1f),ap(ap(c_2Epred__set_2EFUNSET(ty_2Enum_2Enum,arr(A_27a,bool)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),ap(c_2Emeasure_2Esubsets(A_27a),V0a))))) => p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),ap(c_2Epred__set_2EBIGUNION(A_27a),ap(ap(c_2Epred__set_2EIMAGE(ty_2Enum_2Enum,arr(A_27a,bool)),V1f),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)))),ap(c_2Emeasure_2Esubsets(A_27a),V0a))))))))))).
tff(conj_thm_2Emeasure_2EMEASURE__COMPL,lemma,(( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => ((p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) & p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V1s),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V0m)))) => (surj__ty_2Erealax_2Ereal(ap(ap(c_2Emeasure_2Emeasure(A_27a),V0m),ap(ap(c_2Epred__set_2EDIFF(A_27a),ap(c_2Emeasure_2Em__space(A_27a),V0m)),V1s))) = surj__ty_2Erealax_2Ereal(ap(ap(c_2Ereal_2Ereal__sub,ap(ap(c_2Emeasure_2Emeasure(A_27a),V0m),ap(c_2Emeasure_2Em__space(A_27a),V0m))),ap(ap(c_2Emeasure_2Emeasure(A_27a),V0m),V1s)))))))))))).
tff(conj_thm_2Emeasure_2ESIGMA__PROPERTY,lemma,(( ! [A_27a:del]: ( ! [V0sp:$i] : (mem(V0sp,arr(A_27a,bool)) => ( ! [V1p:$i] : (mem(V1p,arr(arr(A_27a,bool),bool)) => ( ! [V2a:$i] : (mem(V2a,arr(arr(A_27a,bool),bool)) => ((p(ap(ap(c_2Emeasure_2Esubset__class(A_27a),V0sp),V1p)) & (p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),c_2Epred__set_2EEMPTY(A_27a)),V1p)) & (p(ap(ap(c_2Epred__set_2ESUBSET(arr(A_27a,bool)),V2a),V1p)) & (( ! [V3s:$i] : (mem(V3s,arr(A_27a,bool)) => (p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V3s),ap(ap(c_2Epred__set_2EINTER(arr(A_27a,bool)),V1p),ap(c_2Emeasure_2Esubsets(A_27a),ap(ap(c_2Emeasure_2Esigma(A_27a),V0sp),V2a))))) => p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),ap(ap(c_2Epred__set_2EDIFF(A_27a),V0sp),V3s)),V1p))))) & ( ! [V4c:$i] : (mem(V4c,arr(arr(A_27a,bool),bool)) => ((p(ap(c_2Epred__set_2Ecountable(arr(A_27a,bool)),V4c)) & p(ap(ap(c_2Epred__set_2ESUBSET(arr(A_27a,bool)),V4c),ap(ap(c_2Epred__set_2EINTER(arr(A_27a,bool)),V1p),ap(c_2Emeasure_2Esubsets(A_27a),ap(ap(c_2Emeasure_2Esigma(A_27a),V0sp),V2a)))))) => p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),ap(c_2Epred__set_2EBIGUNION(A_27a),V4c)),V1p))))))))) => p(ap(ap(c_2Epred__set_2ESUBSET(arr(A_27a,bool)),ap(c_2Emeasure_2Esubsets(A_27a),ap(ap(c_2Emeasure_2Esigma(A_27a),V0sp),V2a))),V1p)))))))))))).
tff(conj_thm_2Emeasure_2EMEASURE__EMPTY,lemma,(( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => (p(ap(c_2Emeasure_2Emeasure__space(A_27a),V0m)) => (surj__ty_2Erealax_2Ereal(ap(ap(c_2Emeasure_2Emeasure(A_27a),V0m),c_2Epred__set_2EEMPTY(A_27a))) = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))))).
tff(conj_thm_2Emeasure_2ESIGMA__SUBSET__MEASURABLE__SETS,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,arr(arr(A_27a,bool),bool)) => ( ! [V1m:$i] : (mem(V1m,ty_2Epair_2Eprod(arr(A_27a,bool),ty_2Epair_2Eprod(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),ty_2Erealax_2Ereal)))) => ((p(ap(c_2Emeasure_2Emeasure__space(A_27a),V1m)) & p(ap(ap(c_2Epred__set_2ESUBSET(arr(A_27a,bool)),V0a),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V1m)))) => p(ap(ap(c_2Epred__set_2ESUBSET(arr(A_27a,bool)),ap(c_2Emeasure_2Esubsets(A_27a),ap(ap(c_2Emeasure_2Esigma(A_27a),ap(c_2Emeasure_2Em__space(A_27a),V1m)),V0a))),ap(c_2Emeasure_2Emeasurable__sets(A_27a),V1m))))))))))).
tff(conj_thm_2Emeasure_2ESIGMA__ALGEBRA__FN,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool))) => (p(ap(c_2Emeasure_2Esigma__algebra(A_27a),V0a)) <=> (p(ap(ap(c_2Emeasure_2Esubset__class(A_27a),ap(c_2Emeasure_2Espace(A_27a),V0a)),ap(c_2Emeasure_2Esubsets(A_27a),V0a))) & (p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),c_2Epred__set_2EEMPTY(A_27a)),ap(c_2Emeasure_2Esubsets(A_27a),V0a))) & (( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => (p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V1s),ap(c_2Emeasure_2Esubsets(A_27a),V0a))) => p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),ap(ap(c_2Epred__set_2EDIFF(A_27a),ap(c_2Emeasure_2Espace(A_27a),V0a)),V1s)),ap(c_2Emeasure_2Esubsets(A_27a),V0a)))))) & ( ! [V2f:$i] : (mem(V2f,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => (p(ap(ap(c_2Ebool_2EIN(arr(ty_2Enum_2Enum,arr(A_27a,bool))),V2f),ap(ap(c_2Epred__set_2EFUNSET(ty_2Enum_2Enum,arr(A_27a,bool)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),ap(c_2Emeasure_2Esubsets(A_27a),V0a)))) => p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),ap(c_2Epred__set_2EBIGUNION(A_27a),ap(ap(c_2Epred__set_2EIMAGE(ty_2Enum_2Enum,arr(A_27a,bool)),V2f),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)))),ap(c_2Emeasure_2Esubsets(A_27a),V0a))))))))))))))).
tff(conj_thm_2Emeasure_2ESIGMA__ALGEBRA__FN__DISJOINT,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool))) => (p(ap(c_2Emeasure_2Esigma__algebra(A_27a),V0a)) <=> (p(ap(ap(c_2Emeasure_2Esubset__class(A_27a),ap(c_2Emeasure_2Espace(A_27a),V0a)),ap(c_2Emeasure_2Esubsets(A_27a),V0a))) & (p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),c_2Epred__set_2EEMPTY(A_27a)),ap(c_2Emeasure_2Esubsets(A_27a),V0a))) & (( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => (p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V1s),ap(c_2Emeasure_2Esubsets(A_27a),V0a))) => p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),ap(ap(c_2Epred__set_2EDIFF(A_27a),ap(c_2Emeasure_2Espace(A_27a),V0a)),V1s)),ap(c_2Emeasure_2Esubsets(A_27a),V0a)))))) & (( ! [V2s:$i] : (mem(V2s,arr(A_27a,bool)) => ( ! [V3t:$i] : (mem(V3t,arr(A_27a,bool)) => ((p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V2s),ap(c_2Emeasure_2Esubsets(A_27a),V0a))) & p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V3t),ap(c_2Emeasure_2Esubsets(A_27a),V0a)))) => p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),ap(ap(c_2Epred__set_2EUNION(A_27a),V2s),V3t)),ap(c_2Emeasure_2Esubsets(A_27a),V0a)))))))) & ( ! [V4f:$i] : (mem(V4f,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ((p(ap(ap(c_2Ebool_2EIN(arr(ty_2Enum_2Enum,arr(A_27a,bool))),V4f),ap(ap(c_2Epred__set_2EFUNSET(ty_2Enum_2Enum,arr(A_27a,bool)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),ap(c_2Emeasure_2Esubsets(A_27a),V0a)))) & ( ! [V5m:tp__ty_2Enum_2Enum] : ( ! [V6n:tp__ty_2Enum_2Enum] : ((~~ (V5m = V6n)) => p(ap(ap(c_2Epred__set_2EDISJOINT(A_27a),ap(V4f,inj__ty_2Enum_2Enum(V5m))),ap(V4f,inj__ty_2Enum_2Enum(V6n)))))))) => p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),ap(c_2Epred__set_2EBIGUNION(A_27a),ap(ap(c_2Epred__set_2EIMAGE(ty_2Enum_2Enum,arr(A_27a,bool)),V4f),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)))),ap(c_2Emeasure_2Esubsets(A_27a),V0a)))))))))))))))).
tff(conj_thm_2Emeasure_2ESIGMA__PROPERTY__ALT,lemma,(( ! [A_27a:del]: ( ! [V0sp:$i] : (mem(V0sp,arr(A_27a,bool)) => ( ! [V1p:$i] : (mem(V1p,arr(arr(A_27a,bool),bool)) => ( ! [V2a:$i] : (mem(V2a,arr(arr(A_27a,bool),bool)) => ((p(ap(ap(c_2Emeasure_2Esubset__class(A_27a),V0sp),V1p)) & (p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),c_2Epred__set_2EEMPTY(A_27a)),V1p)) & (p(ap(ap(c_2Epred__set_2ESUBSET(arr(A_27a,bool)),V2a),V1p)) & (( ! [V3s:$i] : (mem(V3s,arr(A_27a,bool)) => (p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V3s),ap(ap(c_2Epred__set_2EINTER(arr(A_27a,bool)),V1p),ap(c_2Emeasure_2Esubsets(A_27a),ap(ap(c_2Emeasure_2Esigma(A_27a),V0sp),V2a))))) => p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),ap(ap(c_2Epred__set_2EDIFF(A_27a),V0sp),V3s)),V1p))))) & ( ! [V4f:$i] : (mem(V4f,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => (p(ap(ap(c_2Ebool_2EIN(arr(ty_2Enum_2Enum,arr(A_27a,bool))),V4f),ap(ap(c_2Epred__set_2EFUNSET(ty_2Enum_2Enum,arr(A_27a,bool)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),ap(ap(c_2Epred__set_2EINTER(arr(A_27a,bool)),V1p),ap(c_2Emeasure_2Esubsets(A_27a),ap(ap(c_2Emeasure_2Esigma(A_27a),V0sp),V2a)))))) => p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),ap(c_2Epred__set_2EBIGUNION(A_27a),ap(ap(c_2Epred__set_2EIMAGE(ty_2Enum_2Enum,arr(A_27a,bool)),V4f),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)))),V1p))))))))) => p(ap(ap(c_2Epred__set_2ESUBSET(arr(A_27a,bool)),ap(c_2Emeasure_2Esubsets(A_27a),ap(ap(c_2Emeasure_2Esigma(A_27a),V0sp),V2a))),V1p)))))))))))).
tff(conj_thm_2Emeasure_2ESPACE__SMALLEST__CLOSED__CDI,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool))) => (ap(c_2Emeasure_2Espace(A_27a),ap(c_2Emeasure_2Esmallest__closed__cdi(A_27a),V0a)) = ap(c_2Emeasure_2Espace(A_27a),V0a))))))).
tff(conj_thm_2Emeasure_2ESMALLEST__CLOSED__CDI,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool))) => (p(ap(c_2Emeasure_2Ealgebra(A_27a),V0a)) => (p(ap(ap(c_2Epred__set_2ESUBSET(arr(A_27a,bool)),ap(c_2Emeasure_2Esubsets(A_27a),V0a)),ap(c_2Emeasure_2Esubsets(A_27a),ap(c_2Emeasure_2Esmallest__closed__cdi(A_27a),V0a)))) & (p(ap(c_2Emeasure_2Eclosed__cdi(A_27a),ap(c_2Emeasure_2Esmallest__closed__cdi(A_27a),V0a))) & p(ap(ap(c_2Emeasure_2Esubset__class(A_27a),ap(c_2Emeasure_2Espace(A_27a),V0a)),ap(c_2Emeasure_2Esubsets(A_27a),ap(c_2Emeasure_2Esmallest__closed__cdi(A_27a),V0a)))))))))))).
tff(conj_thm_2Emeasure_2ECLOSED__CDI__DUNION,conjecture,(( ! [A_27a:del]: ( ! [V0p:$i] : (mem(V0p,ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool))) => ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => ( ! [V2t:$i] : (mem(V2t,arr(A_27a,bool)) => ((p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),c_2Epred__set_2EEMPTY(A_27a)),ap(c_2Emeasure_2Esubsets(A_27a),V0p))) & (p(ap(c_2Emeasure_2Eclosed__cdi(A_27a),V0p)) & (p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V1s),ap(c_2Emeasure_2Esubsets(A_27a),V0p))) & (p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V2t),ap(c_2Emeasure_2Esubsets(A_27a),V0p))) & p(ap(ap(c_2Epred__set_2EDISJOINT(A_27a),V1s),V2t)))))) => p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),ap(ap(c_2Epred__set_2EUNION(A_27a),V1s),V2t)),ap(c_2Emeasure_2Esubsets(A_27a),V0p))))))))))))).
