include('Axioms/product^2.ax').
thf(tp_c_2Emeasure_2EBorel,type,(c_2Emeasure_2EBorel:$i)).
thf(mem_c_2Emeasure_2EBorel,axiom,(mem@c_2Emeasure_2EBorel@(ty_2Epair_2Eprod@(arr@ty_2Eextreal_2Eextreal@bool)@(arr@(arr@ty_2Eextreal_2Eextreal@bool)@bool)))).
thf(tp_c_2Emeasure_2Eadditive,type,(c_2Emeasure_2Eadditive:(del>$i))).
thf(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)))).
thf(tp_c_2Emeasure_2Ealgebra,type,(c_2Emeasure_2Ealgebra:(del>$i))).
thf(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)))).
thf(tp_c_2Emeasure_2Eclosed__cdi,type,(c_2Emeasure_2Eclosed__cdi:(del>$i))).
thf(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)))).
thf(tp_c_2Emeasure_2Ecountably__additive,type,(c_2Emeasure_2Ecountably__additive:(del>$i))).
thf(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)))).
thf(tp_c_2Emeasure_2Ecountably__subadditive,type,(c_2Emeasure_2Ecountably__subadditive:(del>$i))).
thf(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)))).
thf(tp_c_2Emeasure_2Efn__abs,type,(c_2Emeasure_2Efn__abs:(del>$i))).
thf(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))))).
thf(tp_c_2Emeasure_2Efn__minus,type,(c_2Emeasure_2Efn__minus:(del>$i))).
thf(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))))).
thf(tp_c_2Emeasure_2Efn__plus,type,(c_2Emeasure_2Efn__plus:(del>$i))).
thf(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))))).
thf(tp_c_2Emeasure_2Eincreasing,type,(c_2Emeasure_2Eincreasing:(del>$i))).
thf(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)))).
thf(tp_c_2Emeasure_2Eindicator__fn,type,(c_2Emeasure_2Eindicator__fn:(del>$i))).
thf(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))))).
thf(tp_c_2Emeasure_2Einf__measure,type,(c_2Emeasure_2Einf__measure:(del>$i))).
thf(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))))).
thf(tp_c_2Emeasure_2Elambda__system,type,(c_2Emeasure_2Elambda__system:(del>$i))).
thf(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)))))).
thf(tp_c_2Emeasure_2Em__space,type,(c_2Emeasure_2Em__space:(del>$i))).
thf(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))))).
thf(tp_c_2Emeasure_2Emeasurable,type,(c_2Emeasure_2Emeasurable:(del>(del>$i)))).
thf(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))))))).
thf(tp_c_2Emeasure_2Emeasurable__sets,type,(c_2Emeasure_2Emeasurable__sets:(del>$i))).
thf(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))))).
thf(tp_c_2Emeasure_2Emeasure,type,(c_2Emeasure_2Emeasure:(del>$i))).
thf(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))))).
thf(tp_c_2Emeasure_2Emeasure__preserving,type,(c_2Emeasure_2Emeasure__preserving:(del>(del>$i)))).
thf(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))))))).
thf(tp_c_2Emeasure_2Emeasure__space,type,(c_2Emeasure_2Emeasure__space:(del>$i))).
thf(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)))).
thf(tp_c_2Emeasure_2Enull__set,type,(c_2Emeasure_2Enull__set:(del>$i))).
thf(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))))).
thf(tp_c_2Emeasure_2Eouter__measure__space,type,(c_2Emeasure_2Eouter__measure__space:(del>$i))).
thf(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)))).
thf(tp_c_2Emeasure_2Epos__simple__fn,type,(c_2Emeasure_2Epos__simple__fn:(del>$i))).
thf(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)))))))).
thf(tp_c_2Emeasure_2Epositive,type,(c_2Emeasure_2Epositive:(del>$i))).
thf(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)))).
thf(tp_c_2Emeasure_2Esigma,type,(c_2Emeasure_2Esigma:(del>$i))).
thf(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))))))).
thf(tp_c_2Emeasure_2Esigma__algebra,type,(c_2Emeasure_2Esigma__algebra:(del>$i))).
thf(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)))).
thf(tp_c_2Emeasure_2Esmallest__closed__cdi,type,(c_2Emeasure_2Esmallest__closed__cdi:(del>$i))).
thf(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)))))).
thf(tp_c_2Emeasure_2Espace,type,(c_2Emeasure_2Espace:(del>$i))).
thf(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))))).
thf(tp_c_2Emeasure_2Esubadditive,type,(c_2Emeasure_2Esubadditive:(del>$i))).
thf(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)))).
thf(tp_c_2Emeasure_2Esubset__class,type,(c_2Emeasure_2Esubset__class:(del>$i))).
thf(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))))).
thf(tp_c_2Emeasure_2Esubsets,type,(c_2Emeasure_2Esubsets:(del>$i))).
thf(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))))).
thf(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))))))).
thf(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))))))).
thf(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)))))))))))).
thf(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)))))))))))))))).
thf(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)))))))))))).
thf(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))@(lam@(arr@(arr@A_27a@bool)@bool)@(^ [V2s:$i] : (ap@(ap@(c_2Epair_2E_2C@(arr@(arr@A_27a@bool)@bool)@bool)@V2s)@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Epred__set_2ESUBSET@(arr@A_27a@bool))@V1st)@V2s))@(ap@(c_2Emeasure_2Esigma__algebra@A_27a)@(ap@(ap@(c_2Epair_2E_2C@(arr@A_27a@bool)@(arr@(arr@A_27a@bool)@bool))@V0sp)@V2s)))))))))))))))).
thf(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))))))))).
thf(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))))))))).
thf(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))))))))).
thf(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)))))))))))).
thf(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)))))))))))))).
thf(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)))))))))))))).
thf(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)))))))))))))).
thf(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)))))))))))).
thf(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))))))))))))).
thf(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))))))))).
thf(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))@(lam@(arr@A_27a@bool)@(^ [V2l:$i] : (ap@(ap@(c_2Epair_2E_2C@(arr@A_27a@bool)@bool)@V2l)@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@bool))@V2l)@(ap@(c_2Emeasure_2Esubsets@A_27a)@V0gen)))@(ap@(c_2Ebool_2E_21@(arr@A_27a@bool))@(lam@(arr@A_27a@bool)@(^ [V3s:$i] : (ap@(ap@c_2Emin_2E_3D_3D_3E@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@bool))@V3s)@(ap@(c_2Emeasure_2Esubsets@A_27a)@V0gen)))@(ap@(ap@(c_2Emin_2E_3D@ty_2Erealax_2Ereal)@(ap@(ap@c_2Erealax_2Ereal__add@(ap@V1lam@(ap@(ap@(c_2Epred__set_2EINTER@A_27a)@V2l)@V3s)))@(ap@V1lam@(ap@(ap@(c_2Epred__set_2EINTER@A_27a)@(ap@(ap@(c_2Epred__set_2EDIFF@A_27a)@(ap@(c_2Emeasure_2Espace@A_27a)@V0gen))@V2l))@V3s))))@(ap@V1lam@V3s)))))))))))))))))).
thf(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))))))))).
thf(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)@(lam@ty_2Erealax_2Ereal@(^ [V2r:$i] : (ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@bool)@V2r)@(ap@(c_2Ebool_2E_3F@(arr@ty_2Enum_2Enum@(arr@A_27a@bool)))@(lam@(arr@ty_2Enum_2Enum@(arr@A_27a@bool))@(^ [V3f:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(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))))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(c_2Ebool_2E_21@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V4m:$i] : (ap@(c_2Ebool_2E_21@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V5n:$i] : (ap@(ap@c_2Emin_2E_3D_3D_3E@(ap@c_2Ebool_2E_7E@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@V4m)@V5n)))@(ap@(ap@(c_2Epred__set_2EDISJOINT@A_27a)@(ap@V3f@V4m))@(ap@V3f@V5n))))))))))@(ap@(ap@c_2Ebool_2E_2F_5C@(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)))))@(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))@V2r)))))))))))))))))))).
thf(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)))))))))))))).
thf(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))@(lam@(arr@(arr@A_27a@bool)@bool)@(^ [V1b:$i] : (ap@(ap@(c_2Epair_2E_2C@(arr@(arr@A_27a@bool)@bool)@bool)@V1b)@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Epred__set_2ESUBSET@(arr@A_27a@bool))@(ap@(c_2Emeasure_2Esubsets@A_27a)@V0a))@V1b))@(ap@(c_2Emeasure_2Eclosed__cdi@A_27a)@(ap@(ap@(c_2Epair_2E_2C@(arr@A_27a@bool)@(arr@(arr@A_27a@bool)@bool))@(ap@(c_2Emeasure_2Espace@A_27a)@V0a))@V1b)))))))))))))).
thf(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))@(lam@(arr@A_27a@A_27b)@(^ [V2f:$i] : (ap@(ap@(c_2Epair_2E_2C@(arr@A_27a@A_27b)@bool)@V2f)@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(c_2Emeasure_2Esigma__algebra@A_27a)@V0a))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(c_2Emeasure_2Esigma__algebra@A_27b)@V1b))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@A_27b))@V2f)@(ap@(ap@(c_2Epred__set_2EFUNSET@A_27a@A_27b)@(ap@(c_2Emeasure_2Espace@A_27a)@V0a))@(ap@(c_2Emeasure_2Espace@A_27b)@V1b))))@(ap@(c_2Ebool_2E_21@(arr@A_27b@bool))@(lam@(arr@A_27b@bool)@(^ [V3s:$i] : (ap@(ap@c_2Emin_2E_3D_3D_3E@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27b@bool))@V3s)@(ap@(c_2Emeasure_2Esubsets@A_27b)@V1b)))@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@bool))@(ap@(ap@(c_2Epred__set_2EINTER@A_27a)@(ap@(ap@(c_2Epred__set_2EPREIMAGE@A_27a@A_27b)@V2f)@V3s))@(ap@(c_2Emeasure_2Espace@A_27a)@V0a)))@(ap@(c_2Emeasure_2Esubsets@A_27a)@V0a))))))))))))))))))))).
thf(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))@(lam@(arr@A_27a@A_27b)@(^ [V2f:$i] : (ap@(ap@(c_2Epair_2E_2C@(arr@A_27a@A_27b)@bool)@V2f)@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@A_27b))@V2f)@(ap@(ap@(c_2Emeasure_2Emeasurable@A_27a@A_27b)@(ap@(ap@(c_2Epair_2E_2C@(arr@A_27a@bool)@(arr@(arr@A_27a@bool)@bool))@(ap@(c_2Emeasure_2Em__space@A_27a)@V0m1))@(ap@(c_2Emeasure_2Emeasurable__sets@A_27a)@V0m1)))@(ap@(ap@(c_2Epair_2E_2C@(arr@A_27b@bool)@(arr@(arr@A_27b@bool)@bool))@(ap@(c_2Emeasure_2Em__space@A_27b)@V1m2))@(ap@(c_2Emeasure_2Emeasurable__sets@A_27b)@V1m2)))))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(c_2Emeasure_2Emeasure__space@A_27a)@V0m1))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(c_2Emeasure_2Emeasure__space@A_27b)@V1m2))@(ap@(c_2Ebool_2E_21@(arr@A_27b@bool))@(lam@(arr@A_27b@bool)@(^ [V3s:$i] : (ap@(ap@c_2Emin_2E_3D_3D_3E@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27b@bool))@V3s)@(ap@(c_2Emeasure_2Emeasurable__sets@A_27b)@V1m2)))@(ap@(ap@(c_2Emin_2E_3D@ty_2Erealax_2Ereal)@(ap@(ap@(c_2Emeasure_2Emeasure@A_27a)@V0m1)@(ap@(ap@(c_2Epred__set_2EINTER@A_27a)@(ap@(ap@(c_2Epred__set_2EPREIMAGE@A_27a@A_27b)@V2f)@V3s))@(ap@(c_2Emeasure_2Em__space@A_27a)@V0m1))))@(ap@(ap@(c_2Emeasure_2Emeasure@A_27b)@V1m2)@V3s))))))))))))))))))))).
thf(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) = (lam@A_27a@(^ [V1x:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Eextreal_2Eextreal)@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V1x)@V0s))@(ap@c_2Eextreal_2Eextreal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(ap@c_2Eextreal_2Eextreal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))))))).
thf(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)@(lam@ty_2Enum_2Enum@(^ [V7i:$i] : (ap@(ap@c_2Eextreal_2Eextreal__mul@(ap@c_2Eextreal_2ENormal@(ap@V4x@V7i)))@(ap@(ap@(c_2Emeasure_2Eindicator__fn@A_27a)@(ap@V3a@V7i))@V6t)))))@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))))))))))))))))))))).
thf(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)))))))))))).
thf(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))))).
thf(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)))))))))))))))).
thf(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)))))))).
thf(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)))))))).
thf(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)))))))))).
thf(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)))))))))))).
thf(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)))))))))))).
thf(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)))))))))))).
thf(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)))))))))).
thf(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))))))))).
thf(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)))))))))).
thf(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)))))))))))).
thf(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)))))))))))))).
thf(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))))))))))).
thf(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)))))))))))))))))).
thf(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))))))))))))))))).
thf(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))))))).
thf(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)))))))))))).
thf(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)))))))))))).
thf(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)))))))))))).
thf(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))))))))))))))).
thf(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))))))))))))))).
thf(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))))))))))))).
thf(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))))))))))))))).
thf(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)))))))))).
thf(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))))))))))).
thf(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))))))))))).
thf(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))@(lam@(arr@A_27a@bool)@(^ [V7s:$i] : (ap@(ap@(c_2Epred__set_2EINTER@A_27a)@V7s)@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)))))))))))))))).
thf(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))))))).
thf(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))))))).
thf(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))))))))))))))))).
thf(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))))))))))).
thf(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)@(lam@ty_2Erealax_2Ereal@(^ [V3r:$i] : (ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@bool)@V3r)@(ap@(c_2Ebool_2E_3F@(arr@ty_2Enum_2Enum@(arr@A_27a@bool)))@(lam@(arr@ty_2Enum_2Enum@(arr@A_27a@bool))@(^ [V4f:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(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_2Emeasurable__sets@A_27a)@V0m))))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(c_2Ebool_2E_21@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V5m:$i] : (ap@(c_2Ebool_2E_21@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V6n:$i] : (ap@(ap@c_2Emin_2E_3D_3D_3E@(ap@c_2Ebool_2E_7E@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@V5m)@V6n)))@(ap@(ap@(c_2Epred__set_2EDISJOINT@A_27a)@(ap@V4f@V5m))@(ap@V4f@V6n))))))))))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V1g)@(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@(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))@V4f))@V3r)))))))))))))))))))))).
thf(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)@(lam@ty_2Erealax_2Ereal@(^ [V3r:$i] : (ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@bool)@V3r)@(ap@(c_2Ebool_2E_3F@(arr@ty_2Enum_2Enum@(arr@A_27a@bool)))@(lam@(arr@ty_2Enum_2Enum@(arr@A_27a@bool))@(^ [V4f:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(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_2Emeasurable__sets@A_27a)@V0m))))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(c_2Ebool_2E_21@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V5m:$i] : (ap@(c_2Ebool_2E_21@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V6n:$i] : (ap@(ap@c_2Emin_2E_3D_3D_3E@(ap@c_2Ebool_2E_7E@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@V5m)@V6n)))@(ap@(ap@(c_2Epred__set_2EDISJOINT@A_27a)@(ap@V4f@V5m))@(ap@V4f@V6n))))))))))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V1g)@(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@(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))@V4f))@V3r))))))))))))))) => (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))))))))))).
thf(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)))))))))).
thf(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)))))))))))).
thf(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))))))).
thf(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))))))).
thf(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)))))))))))).
thf(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)))))))))).
thf(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))))))))).
thf(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)))))))))).
thf(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)))))))).
thf(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)))))))).
thf(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))))))).
thf(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))))))))).
thf(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)))))))))).
thf(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)))))))))).
thf(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)@(lam@ty_2Erealax_2Ereal@(^ [V3r:$i] : (ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@bool)@V3r)@(ap@(c_2Ebool_2E_3F@(arr@ty_2Enum_2Enum@(arr@A_27a@bool)))@(lam@(arr@ty_2Enum_2Enum@(arr@A_27a@bool))@(^ [V4f:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(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_2Emeasurable__sets@A_27a)@V0m))))@(ap@(ap@c_2Ebool_2E_2F_5C@(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))@V4f)@(c_2Epred__set_2EUNIV@ty_2Enum_2Enum)))))@(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))@V4f))@V3r))))))))))))))) => (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@(ap@(c_2Emeasure_2Einf__measure@A_27a)@V0m)@V1s))@(inj__ty_2Erealax_2Ereal @ V2x))))))))))).
thf(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))))))))))))))))))).
thf(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)))))))))).
thf(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)))))))))).
thf(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)))))))))).
thf(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))))))))).
thf(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))))))))))).
thf(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)))))))))).
thf(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))))))))))))).
thf(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)))))))))))))).
thf(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)))))))))).
thf(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)))))))))).
thf(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))))))))))).
thf(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))))))))))).
thf(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))))))))).
thf(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)))))))))).
thf(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)))))))))))))).
thf(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))))))))))))))).
thf(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))))))))))).
thf(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)))))).
thf(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))))))))))).
thf(conj_thm_2Emeasure_2ECLOSED__CDI__DUNION,lemma,( ! [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)))))))))))).
thf(conj_thm_2Emeasure_2ECLOSED__CDI__COMPL,lemma,( ! [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)) => (((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))@(ap@(ap@(c_2Epred__set_2EDIFF@A_27a)@(ap@(c_2Emeasure_2Espace@A_27a)@V0p))@V1s))@(ap@(c_2Emeasure_2Esubsets@A_27a)@V0p)))))))))).
thf(conj_thm_2Emeasure_2ECLOSED__CDI__DISJOINT,lemma,( ! [A_27a:del]: ( ! [V0p:$i] : ((mem@V0p@(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_2Eclosed__cdi@A_27a)@V0p)) & ((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)@V0p)))) & ( ! [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)@V0p)))))))))).
thf(conj_thm_2Emeasure_2ECLOSED__CDI__INCREASING,lemma,( ! [A_27a:del]: ( ! [V0p:$i] : ((mem@V0p@(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_2Eclosed__cdi@A_27a)@V0p)) & ((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)@V0p)))) & (((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)@V0p)))))))))).
thf(conj_thm_2Emeasure_2ESIGMA__PROPERTY__DISJOINT__LEMMA1,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)) => ( ! [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_2Esubsets@A_27a)@V0a))) & (p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@bool))@V2t)@(ap@(c_2Emeasure_2Esubsets@A_27a)@(ap@(c_2Emeasure_2Esmallest__closed__cdi@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)@(ap@(c_2Emeasure_2Esmallest__closed__cdi@A_27a)@V0a)))))))))))))).
thf(conj_thm_2Emeasure_2ESIGMA__PROPERTY__DISJOINT__LEMMA2,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)) => ( ! [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_2Esubsets@A_27a)@(ap@(c_2Emeasure_2Esmallest__closed__cdi@A_27a)@V0a)))) & (p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@bool))@V2t)@(ap@(c_2Emeasure_2Esubsets@A_27a)@(ap@(c_2Emeasure_2Esmallest__closed__cdi@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)@(ap@(c_2Emeasure_2Esmallest__closed__cdi@A_27a)@V0a)))))))))))))).
thf(conj_thm_2Emeasure_2ESIGMA__PROPERTY__DISJOINT__LEMMA,lemma,( ! [A_27a:del]: ( ! [V0sp:$i] : ((mem@V0sp@(arr@A_27a@bool)) => ( ! [V1a:$i] : ((mem@V1a@(arr@(arr@A_27a@bool)@bool)) => ( ! [V2p:$i] : ((mem@V2p@(arr@(arr@A_27a@bool)@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)@V1a))) & ((p@(ap@(ap@(c_2Epred__set_2ESUBSET@(arr@A_27a@bool))@V1a)@V2p)) & (p@(ap@(c_2Emeasure_2Eclosed__cdi@A_27a)@(ap@(ap@(c_2Epair_2E_2C@(arr@A_27a@bool)@(arr@(arr@A_27a@bool)@bool))@V0sp)@V2p))))) => (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)@V1a)))@V2p))))))))))).
thf(conj_thm_2Emeasure_2ESIGMA__PROPERTY__DISJOINT__WEAK,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@(c_2Emeasure_2Ealgebra@A_27a)@(ap@(ap@(c_2Epair_2E_2C@(arr@A_27a@bool)@(arr@(arr@A_27a@bool)@bool))@V0sp)@V2a))) & ((p@(ap@(ap@(c_2Epred__set_2ESUBSET@(arr@A_27a@bool))@V2a)@V1p)) & ((p@(ap@(ap@(c_2Emeasure_2Esubset__class@A_27a)@V0sp)@V1p)) & (( ! [V3s:$i] : ((mem@V3s@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@bool))@V3s)@V1p)) => (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))@V1p))) & (((ap@V4f@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)) = (c_2Epred__set_2EEMPTY@A_27a)) & ( ! [V5n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@(ap@V4f@(inj__ty_2Enum_2Enum @ V5n)))@(ap@V4f@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V5n)))))))) => (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))))) & ( ! [V6f:$i] : ((mem@V6f@(arr@ty_2Enum_2Enum@(arr@A_27a@bool))) => (((p@(ap@(ap@(c_2Ebool_2EIN@(arr@ty_2Enum_2Enum@(arr@A_27a@bool)))@V6f)@(ap@(ap@(c_2Epred__set_2EFUNSET@ty_2Enum_2Enum@(arr@A_27a@bool))@(c_2Epred__set_2EUNIV@ty_2Enum_2Enum))@V1p))) & ( ! [V7m:tp__ty_2Enum_2Enum] : ( ! [V8n:tp__ty_2Enum_2Enum] : ((~~ (V7m = V8n)) => (p@(ap@(ap@(c_2Epred__set_2EDISJOINT@A_27a)@(ap@V6f@(inj__ty_2Enum_2Enum @ V7m)))@(ap@V6f@(inj__ty_2Enum_2Enum @ V8n)))))))) => (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))@V6f)@(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))))))))))).
thf(conj_thm_2Emeasure_2ESIGMA__PROPERTY__DISJOINT,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@(c_2Emeasure_2Ealgebra@A_27a)@(ap@(ap@(c_2Epair_2E_2C@(arr@A_27a@bool)@(arr@(arr@A_27a@bool)@bool))@V0sp)@V2a))) & ((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)))))) & (((ap@V4f@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)) = (c_2Epred__set_2EEMPTY@A_27a)) & ( ! [V5n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@(ap@V4f@(inj__ty_2Enum_2Enum @ V5n)))@(ap@V4f@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V5n)))))))) => (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))))) & ( ! [V6f:$i] : ((mem@V6f@(arr@ty_2Enum_2Enum@(arr@A_27a@bool))) => (((p@(ap@(ap@(c_2Ebool_2EIN@(arr@ty_2Enum_2Enum@(arr@A_27a@bool)))@V6f)@(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)))))) & ( ! [V7m:tp__ty_2Enum_2Enum] : ( ! [V8n:tp__ty_2Enum_2Enum] : ((~~ (V7m = V8n)) => (p@(ap@(ap@(c_2Epred__set_2EDISJOINT@A_27a)@(ap@V6f@(inj__ty_2Enum_2Enum @ V7m)))@(ap@V6f@(inj__ty_2Enum_2Enum @ V8n)))))))) => (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))@V6f)@(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))))))))))).
thf(conj_thm_2Emeasure_2EMEASURE__COUNTABLY__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_2Emeasure__space@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_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)))))))))))).
thf(conj_thm_2Emeasure_2EMEASURE__SPACE__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_2Emeasure__space@A_27a)@V0m)) => (p@(ap@(c_2Emeasure_2Eadditive@A_27a)@V0m))))))).
thf(conj_thm_2Emeasure_2EMEASURE__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)) => ( ! [V2t:$i] : ((mem@V2t@(arr@A_27a@bool)) => ( ! [V3u:$i] : ((mem@V3u@(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))) & ((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))))))))))))))).
thf(conj_thm_2Emeasure_2EMEASURE__COUNTABLE__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)))) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2f:$i] : ((mem@V2f@(arr@ty_2Enum_2Enum@(arr@A_27a@bool))) => (((p@(ap@(c_2Emeasure_2Emeasure__space@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)))) & (((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)))))) & (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_2Eseq_2E_2D_2D_3E@(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)))))))))))).
thf(conj_thm_2Emeasure_2EMEASURE__SPACE__REDUCE,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)))) => ((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_2Emeasure_2Emeasurable__sets@A_27a)@V0m))@(ap@(c_2Emeasure_2Emeasure@A_27a)@V0m))) = V0m))))).
thf(conj_thm_2Emeasure_2ESPACE__SIGMA,lemma,( ! [A_27a:del]: ( ! [V0sp:$i] : ((mem@V0sp@(arr@A_27a@bool)) => ( ! [V1a:$i] : ((mem@V1a@(arr@(arr@A_27a@bool)@bool)) => ((ap@(c_2Emeasure_2Espace@A_27a)@(ap@(ap@(c_2Emeasure_2Esigma@A_27a)@V0sp)@V1a)) = V0sp))))))).
thf(conj_thm_2Emeasure_2EMONOTONE__CONVERGENCE,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_2Emeasure__space@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)))) & (( ! [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)))))) & (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_2Eseq_2E_2D_2D_3E@(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)))))))))))).
thf(conj_thm_2Emeasure_2ESIGMA__REDUCE,lemma,( ! [A_27a:del]: ( ! [V0sp:$i] : ((mem@V0sp@(arr@A_27a@bool)) => ( ! [V1a:$i] : ((mem@V1a@(arr@(arr@A_27a@bool)@bool)) => ((ap@(ap@(c_2Epair_2E_2C@(arr@A_27a@bool)@(arr@(arr@A_27a@bool)@bool))@V0sp)@(ap@(c_2Emeasure_2Esubsets@A_27a)@(ap@(ap@(c_2Emeasure_2Esigma@A_27a)@V0sp)@V1a))) = (ap@(ap@(c_2Emeasure_2Esigma@A_27a)@V0sp)@V1a)))))))).
thf(conj_thm_2Emeasure_2EMEASURABLE__SETS__SUBSET__SPACE,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)))) => (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V1s)@(ap@(c_2Emeasure_2Em__space@A_27a)@V0m)))))))))).
thf(conj_thm_2Emeasure_2EMEASURABLE__DIFF__PROPERTY,lemma,( ! [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))) => ( ! [V2f:$i] : ((mem@V2f@(arr@A_27a@A_27b)) => (((p@(ap@(c_2Emeasure_2Esigma__algebra@A_27a)@V0a)) & ((p@(ap@(c_2Emeasure_2Esigma__algebra@A_27b)@V1b)) & ((p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@A_27b))@V2f)@(ap@(ap@(c_2Epred__set_2EFUNSET@A_27a@A_27b)@(ap@(c_2Emeasure_2Espace@A_27a)@V0a))@(ap@(c_2Emeasure_2Espace@A_27b)@V1b)))) & ( ! [V3s:$i] : ((mem@V3s@(arr@A_27b@bool)) => ((p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27b@bool))@V3s)@(ap@(c_2Emeasure_2Esubsets@A_27b)@V1b))) => (p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@bool))@(ap@(ap@(c_2Epred__set_2EPREIMAGE@A_27a@A_27b)@V2f)@V3s))@(ap@(c_2Emeasure_2Esubsets@A_27a)@V0a))))))))) => ( ! [V4s:$i] : ((mem@V4s@(arr@A_27b@bool)) => ((p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27b@bool))@V4s)@(ap@(c_2Emeasure_2Esubsets@A_27b)@V1b))) => ((ap@(ap@(c_2Epred__set_2EPREIMAGE@A_27a@A_27b)@V2f)@(ap@(ap@(c_2Epred__set_2EDIFF@A_27b)@(ap@(c_2Emeasure_2Espace@A_27b)@V1b))@V4s)) = (ap@(ap@(c_2Epred__set_2EDIFF@A_27a)@(ap@(c_2Emeasure_2Espace@A_27a)@V0a))@(ap@(ap@(c_2Epred__set_2EPREIMAGE@A_27a@A_27b)@V2f)@V4s)))))))))))))))).
thf(conj_thm_2Emeasure_2EMEASURABLE__BIGUNION__PROPERTY,lemma,( ! [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))) => ( ! [V2f:$i] : ((mem@V2f@(arr@A_27a@A_27b)) => (((p@(ap@(c_2Emeasure_2Esigma__algebra@A_27a)@V0a)) & ((p@(ap@(c_2Emeasure_2Esigma__algebra@A_27b)@V1b)) & ((p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@A_27b))@V2f)@(ap@(ap@(c_2Epred__set_2EFUNSET@A_27a@A_27b)@(ap@(c_2Emeasure_2Espace@A_27a)@V0a))@(ap@(c_2Emeasure_2Espace@A_27b)@V1b)))) & ( ! [V3s:$i] : ((mem@V3s@(arr@A_27b@bool)) => ((p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27b@bool))@V3s)@(ap@(c_2Emeasure_2Esubsets@A_27b)@V1b))) => (p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@bool))@(ap@(ap@(c_2Epred__set_2EPREIMAGE@A_27a@A_27b)@V2f)@V3s))@(ap@(c_2Emeasure_2Esubsets@A_27a)@V0a))))))))) => ( ! [V4c:$i] : ((mem@V4c@(arr@(arr@A_27b@bool)@bool)) => ((p@(ap@(ap@(c_2Epred__set_2ESUBSET@(arr@A_27b@bool))@V4c)@(ap@(c_2Emeasure_2Esubsets@A_27b)@V1b))) => ((ap@(ap@(c_2Epred__set_2EPREIMAGE@A_27a@A_27b)@V2f)@(ap@(c_2Epred__set_2EBIGUNION@A_27b)@V4c)) = (ap@(c_2Epred__set_2EBIGUNION@A_27a)@(ap@(ap@(c_2Epred__set_2EIMAGE@(arr@A_27b@bool)@(arr@A_27a@bool))@(ap@(c_2Epred__set_2EPREIMAGE@A_27a@A_27b)@V2f))@V4c)))))))))))))))).
thf(conj_thm_2Emeasure_2EMEASUBABLE__BIGUNION__LEMMA,lemma,( ! [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))) => ( ! [V2f:$i] : ((mem@V2f@(arr@A_27a@A_27b)) => (((p@(ap@(c_2Emeasure_2Esigma__algebra@A_27a)@V0a)) & ((p@(ap@(c_2Emeasure_2Esigma__algebra@A_27b)@V1b)) & ((p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@A_27b))@V2f)@(ap@(ap@(c_2Epred__set_2EFUNSET@A_27a@A_27b)@(ap@(c_2Emeasure_2Espace@A_27a)@V0a))@(ap@(c_2Emeasure_2Espace@A_27b)@V1b)))) & ( ! [V3s:$i] : ((mem@V3s@(arr@A_27b@bool)) => ((p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27b@bool))@V3s)@(ap@(c_2Emeasure_2Esubsets@A_27b)@V1b))) => (p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@bool))@(ap@(ap@(c_2Epred__set_2EPREIMAGE@A_27a@A_27b)@V2f)@V3s))@(ap@(c_2Emeasure_2Esubsets@A_27a)@V0a))))))))) => ( ! [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_2EIMAGE@(arr@A_27b@bool)@(arr@A_27a@bool))@(ap@(c_2Epred__set_2EPREIMAGE@A_27a@A_27b)@V2f))@(ap@(c_2Emeasure_2Esubsets@A_27b)@V1b))))) => (p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@bool))@(ap@(c_2Epred__set_2EBIGUNION@A_27a)@V4c))@(ap@(ap@(c_2Epred__set_2EIMAGE@(arr@A_27b@bool)@(arr@A_27a@bool))@(ap@(c_2Epred__set_2EPREIMAGE@A_27a@A_27b)@V2f))@(ap@(c_2Emeasure_2Esubsets@A_27b)@V1b))))))))))))))))).
thf(conj_thm_2Emeasure_2EMEASURABLE__SIGMA__PREIMAGES,lemma,( ! [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))) => ( ! [V2f:$i] : ((mem@V2f@(arr@A_27a@A_27b)) => (((p@(ap@(c_2Emeasure_2Esigma__algebra@A_27a)@V0a)) & ((p@(ap@(c_2Emeasure_2Esigma__algebra@A_27b)@V1b)) & ((p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@A_27b))@V2f)@(ap@(ap@(c_2Epred__set_2EFUNSET@A_27a@A_27b)@(ap@(c_2Emeasure_2Espace@A_27a)@V0a))@(ap@(c_2Emeasure_2Espace@A_27b)@V1b)))) & ( ! [V3s:$i] : ((mem@V3s@(arr@A_27b@bool)) => ((p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27b@bool))@V3s)@(ap@(c_2Emeasure_2Esubsets@A_27b)@V1b))) => (p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@bool))@(ap@(ap@(c_2Epred__set_2EPREIMAGE@A_27a@A_27b)@V2f)@V3s))@(ap@(c_2Emeasure_2Esubsets@A_27a)@V0a))))))))) => (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_2Espace@A_27a)@V0a))@(ap@(ap@(c_2Epred__set_2EIMAGE@(arr@A_27b@bool)@(arr@A_27a@bool))@(ap@(c_2Epred__set_2EPREIMAGE@A_27a@A_27b)@V2f))@(ap@(c_2Emeasure_2Esubsets@A_27b)@V1b))))))))))))))).
thf(conj_thm_2Emeasure_2EIN__MEASURABLE,lemma,( ! [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))) => ( ! [V2f:$i] : ((mem@V2f@(arr@A_27a@A_27b)) => ((p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@A_27b))@V2f)@(ap@(ap@(c_2Emeasure_2Emeasurable@A_27a@A_27b)@V0a)@V1b))) <=> ((p@(ap@(c_2Emeasure_2Esigma__algebra@A_27a)@V0a)) & ((p@(ap@(c_2Emeasure_2Esigma__algebra@A_27b)@V1b)) & ((p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@A_27b))@V2f)@(ap@(ap@(c_2Epred__set_2EFUNSET@A_27a@A_27b)@(ap@(c_2Emeasure_2Espace@A_27a)@V0a))@(ap@(c_2Emeasure_2Espace@A_27b)@V1b)))) & ( ! [V3s:$i] : ((mem@V3s@(arr@A_27b@bool)) => ((p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27b@bool))@V3s)@(ap@(c_2Emeasure_2Esubsets@A_27b)@V1b))) => (p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@bool))@(ap@(ap@(c_2Epred__set_2EINTER@A_27a)@(ap@(ap@(c_2Epred__set_2EPREIMAGE@A_27a@A_27b)@V2f)@V3s))@(ap@(c_2Emeasure_2Espace@A_27a)@V0a)))@(ap@(c_2Emeasure_2Esubsets@A_27a)@V0a))))))))))))))))))).
thf(conj_thm_2Emeasure_2EMEASURABLE__SIGMA,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1a:$i] : ((mem@V1a@(ty_2Epair_2Eprod@(arr@A_27a@bool)@(arr@(arr@A_27a@bool)@bool))) => ( ! [V2b:$i] : ((mem@V2b@(arr@(arr@A_27b@bool)@bool)) => ( ! [V3sp:$i] : ((mem@V3sp@(arr@A_27b@bool)) => (((p@(ap@(c_2Emeasure_2Esigma__algebra@A_27a)@V1a)) & ((p@(ap@(ap@(c_2Emeasure_2Esubset__class@A_27b)@V3sp)@V2b)) & ((p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@A_27b))@V0f)@(ap@(ap@(c_2Epred__set_2EFUNSET@A_27a@A_27b)@(ap@(c_2Emeasure_2Espace@A_27a)@V1a))@V3sp))) & ( ! [V4s:$i] : ((mem@V4s@(arr@A_27b@bool)) => ((p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27b@bool))@V4s)@V2b)) => (p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@bool))@(ap@(ap@(c_2Epred__set_2EINTER@A_27a)@(ap@(ap@(c_2Epred__set_2EPREIMAGE@A_27a@A_27b)@V0f)@V4s))@(ap@(c_2Emeasure_2Espace@A_27a)@V1a)))@(ap@(c_2Emeasure_2Esubsets@A_27a)@V1a))))))))) => (p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@A_27b))@V0f)@(ap@(ap@(c_2Emeasure_2Emeasurable@A_27a@A_27b)@V1a)@(ap@(ap@(c_2Emeasure_2Esigma@A_27b)@V3sp)@V2b)))))))))))))))).
thf(conj_thm_2Emeasure_2EMEASURABLE__SUBSET,lemma,( ! [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))) => (p@(ap@(ap@(c_2Epred__set_2ESUBSET@(arr@A_27a@A_27b))@(ap@(ap@(c_2Emeasure_2Emeasurable@A_27a@A_27b)@V0a)@V1b))@(ap@(ap@(c_2Emeasure_2Emeasurable@A_27a@A_27b)@V0a)@(ap@(ap@(c_2Emeasure_2Esigma@A_27b)@(ap@(c_2Emeasure_2Espace@A_27b)@V1b))@(ap@(c_2Emeasure_2Esubsets@A_27b)@V1b)))))))))))).
thf(conj_thm_2Emeasure_2EMEASURABLE__LIFT,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1a:$i] : ((mem@V1a@(ty_2Epair_2Eprod@(arr@A_27a@bool)@(arr@(arr@A_27a@bool)@bool))) => ( ! [V2b:$i] : ((mem@V2b@(ty_2Epair_2Eprod@(arr@A_27b@bool)@(arr@(arr@A_27b@bool)@bool))) => ((p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@A_27b))@V0f)@(ap@(ap@(c_2Emeasure_2Emeasurable@A_27a@A_27b)@V1a)@V2b))) => (p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@A_27b))@V0f)@(ap@(ap@(c_2Emeasure_2Emeasurable@A_27a@A_27b)@V1a)@(ap@(ap@(c_2Emeasure_2Esigma@A_27b)@(ap@(c_2Emeasure_2Espace@A_27b)@V2b))@(ap@(c_2Emeasure_2Esubsets@A_27b)@V2b))))))))))))))).
thf(conj_thm_2Emeasure_2EIN__MEASURE__PRESERVING,lemma,( ! [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)))) => ( ! [V2f:$i] : ((mem@V2f@(arr@A_27a@A_27b)) => ((p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@A_27b))@V2f)@(ap@(ap@(c_2Emeasure_2Emeasure__preserving@A_27a@A_27b)@V0m1)@V1m2))) <=> ((p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@A_27b))@V2f)@(ap@(ap@(c_2Emeasure_2Emeasurable@A_27a@A_27b)@(ap@(ap@(c_2Epair_2E_2C@(arr@A_27a@bool)@(arr@(arr@A_27a@bool)@bool))@(ap@(c_2Emeasure_2Em__space@A_27a)@V0m1))@(ap@(c_2Emeasure_2Emeasurable__sets@A_27a)@V0m1)))@(ap@(ap@(c_2Epair_2E_2C@(arr@A_27b@bool)@(arr@(arr@A_27b@bool)@bool))@(ap@(c_2Emeasure_2Em__space@A_27b)@V1m2))@(ap@(c_2Emeasure_2Emeasurable__sets@A_27b)@V1m2))))) & ((p@(ap@(c_2Emeasure_2Emeasure__space@A_27a)@V0m1)) & ((p@(ap@(c_2Emeasure_2Emeasure__space@A_27b)@V1m2)) & ( ! [V3s:$i] : ((mem@V3s@(arr@A_27b@bool)) => ((p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27b@bool))@V3s)@(ap@(c_2Emeasure_2Emeasurable__sets@A_27b)@V1m2))) => ((surj__ty_2Erealax_2Ereal @ (ap@(ap@(c_2Emeasure_2Emeasure@A_27a)@V0m1)@(ap@(ap@(c_2Epred__set_2EINTER@A_27a)@(ap@(ap@(c_2Epred__set_2EPREIMAGE@A_27a@A_27b)@V2f)@V3s))@(ap@(c_2Emeasure_2Em__space@A_27a)@V0m1)))) = (surj__ty_2Erealax_2Ereal @ (ap@(ap@(c_2Emeasure_2Emeasure@A_27b)@V1m2)@V3s))))))))))))))))))).
thf(conj_thm_2Emeasure_2EMEASURE__PRESERVING__LIFT,lemma,( ! [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)))) => ( ! [V2a:$i] : ((mem@V2a@(arr@(arr@A_27b@bool)@bool)) => ( ! [V3f:$i] : ((mem@V3f@(arr@A_27a@A_27b)) => (((p@(ap@(c_2Emeasure_2Emeasure__space@A_27a)@V0m1)) & ((p@(ap@(c_2Emeasure_2Emeasure__space@A_27b)@V1m2)) & (((ap@(c_2Emeasure_2Emeasurable__sets@A_27b)@V1m2) = (ap@(c_2Emeasure_2Esubsets@A_27b)@(ap@(ap@(c_2Emeasure_2Esigma@A_27b)@(ap@(c_2Emeasure_2Em__space@A_27b)@V1m2))@V2a))) & (p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@A_27b))@V3f)@(ap@(ap@(c_2Emeasure_2Emeasure__preserving@A_27a@A_27b)@V0m1)@(ap@(ap@(c_2Epair_2E_2C@(arr@A_27b@bool)@(ty_2Epair_2Eprod@(arr@(arr@A_27b@bool)@bool)@(arr@(arr@A_27b@bool)@ty_2Erealax_2Ereal)))@(ap@(c_2Emeasure_2Em__space@A_27b)@V1m2))@(ap@(ap@(c_2Epair_2E_2C@(arr@(arr@A_27b@bool)@bool)@(arr@(arr@A_27b@bool)@ty_2Erealax_2Ereal))@V2a)@(ap@(c_2Emeasure_2Emeasure@A_27b)@V1m2))))))))) => (p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@A_27b))@V3f)@(ap@(ap@(c_2Emeasure_2Emeasure__preserving@A_27a@A_27b)@V0m1)@V1m2))))))))))))))).
thf(conj_thm_2Emeasure_2EMEASURE__PRESERVING__SUBSET,lemma,( ! [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)))) => ( ! [V2a:$i] : ((mem@V2a@(arr@(arr@A_27b@bool)@bool)) => (((p@(ap@(c_2Emeasure_2Emeasure__space@A_27a)@V0m1)) & ((p@(ap@(c_2Emeasure_2Emeasure__space@A_27b)@V1m2)) & ((ap@(c_2Emeasure_2Emeasurable__sets@A_27b)@V1m2) = (ap@(c_2Emeasure_2Esubsets@A_27b)@(ap@(ap@(c_2Emeasure_2Esigma@A_27b)@(ap@(c_2Emeasure_2Em__space@A_27b)@V1m2))@V2a))))) => (p@(ap@(ap@(c_2Epred__set_2ESUBSET@(arr@A_27a@A_27b))@(ap@(ap@(c_2Emeasure_2Emeasure__preserving@A_27a@A_27b)@V0m1)@(ap@(ap@(c_2Epair_2E_2C@(arr@A_27b@bool)@(ty_2Epair_2Eprod@(arr@(arr@A_27b@bool)@bool)@(arr@(arr@A_27b@bool)@ty_2Erealax_2Ereal)))@(ap@(c_2Emeasure_2Em__space@A_27b)@V1m2))@(ap@(ap@(c_2Epair_2E_2C@(arr@(arr@A_27b@bool)@bool)@(arr@(arr@A_27b@bool)@ty_2Erealax_2Ereal))@V2a)@(ap@(c_2Emeasure_2Emeasure@A_27b)@V1m2)))))@(ap@(ap@(c_2Emeasure_2Emeasure__preserving@A_27a@A_27b)@V0m1)@V1m2))))))))))))).
thf(conj_thm_2Emeasure_2EMEASURABLE__I,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_2Ebool_2EIN@(arr@A_27a@A_27a))@(c_2Ecombin_2EI@A_27a))@(ap@(ap@(c_2Emeasure_2Emeasurable@A_27a@A_27a)@V0a)@V0a)))))))).
thf(conj_thm_2Emeasure_2EMEASURABLE__COMP,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1g:$i] : ((mem@V1g@(arr@A_27b@A_27c)) => ( ! [V2a:$i] : ((mem@V2a@(ty_2Epair_2Eprod@(arr@A_27a@bool)@(arr@(arr@A_27a@bool)@bool))) => ( ! [V3b:$i] : ((mem@V3b@(ty_2Epair_2Eprod@(arr@A_27b@bool)@(arr@(arr@A_27b@bool)@bool))) => ( ! [V4c:$i] : ((mem@V4c@(ty_2Epair_2Eprod@(arr@A_27c@bool)@(arr@(arr@A_27c@bool)@bool))) => (((p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@A_27b))@V0f)@(ap@(ap@(c_2Emeasure_2Emeasurable@A_27a@A_27b)@V2a)@V3b))) & (p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27b@A_27c))@V1g)@(ap@(ap@(c_2Emeasure_2Emeasurable@A_27b@A_27c)@V3b)@V4c)))) => (p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@A_27c))@(ap@(ap@(c_2Ecombin_2Eo@A_27a@A_27c@A_27b)@V1g)@V0f))@(ap@(ap@(c_2Emeasure_2Emeasurable@A_27a@A_27c)@V2a)@V4c)))))))))))))))))).
thf(conj_thm_2Emeasure_2EMEASURABLE__COMP__STRONG,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1g:$i] : ((mem@V1g@(arr@A_27b@A_27c)) => ( ! [V2a:$i] : ((mem@V2a@(ty_2Epair_2Eprod@(arr@A_27a@bool)@(arr@(arr@A_27a@bool)@bool))) => ( ! [V3b:$i] : ((mem@V3b@(ty_2Epair_2Eprod@(arr@A_27b@bool)@(arr@(arr@A_27b@bool)@bool))) => ( ! [V4c:$i] : ((mem@V4c@(ty_2Epair_2Eprod@(arr@A_27c@bool)@(arr@(arr@A_27c@bool)@bool))) => (((p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@A_27b))@V0f)@(ap@(ap@(c_2Emeasure_2Emeasurable@A_27a@A_27b)@V2a)@V3b))) & ((p@(ap@(c_2Emeasure_2Esigma__algebra@A_27c)@V4c)) & ((p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27b@A_27c))@V1g)@(ap@(ap@(c_2Epred__set_2EFUNSET@A_27b@A_27c)@(ap@(c_2Emeasure_2Espace@A_27b)@V3b))@(ap@(c_2Emeasure_2Espace@A_27c)@V4c)))) & ( ! [V5x:$i] : ((mem@V5x@(arr@A_27c@bool)) => ((p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27c@bool))@V5x)@(ap@(c_2Emeasure_2Esubsets@A_27c)@V4c))) => (p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27b@bool))@(ap@(ap@(c_2Epred__set_2EINTER@A_27b)@(ap@(ap@(c_2Epred__set_2EPREIMAGE@A_27b@A_27c)@V1g)@V5x))@(ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V0f)@(ap@(c_2Emeasure_2Espace@A_27a)@V2a))))@(ap@(c_2Emeasure_2Esubsets@A_27b)@V3b))))))))) => (p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@A_27c))@(ap@(ap@(c_2Ecombin_2Eo@A_27a@A_27c@A_27b)@V1g)@V0f))@(ap@(ap@(c_2Emeasure_2Emeasurable@A_27a@A_27c)@V2a)@V4c)))))))))))))))))).
thf(conj_thm_2Emeasure_2EMEASURABLE__COMP__STRONGER,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1g:$i] : ((mem@V1g@(arr@A_27b@A_27c)) => ( ! [V2a:$i] : ((mem@V2a@(ty_2Epair_2Eprod@(arr@A_27a@bool)@(arr@(arr@A_27a@bool)@bool))) => ( ! [V3b:$i] : ((mem@V3b@(ty_2Epair_2Eprod@(arr@A_27b@bool)@(arr@(arr@A_27b@bool)@bool))) => ( ! [V4c:$i] : ((mem@V4c@(ty_2Epair_2Eprod@(arr@A_27c@bool)@(arr@(arr@A_27c@bool)@bool))) => ( ! [V5t:$i] : ((mem@V5t@(arr@A_27b@bool)) => (((p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@A_27b))@V0f)@(ap@(ap@(c_2Emeasure_2Emeasurable@A_27a@A_27b)@V2a)@V3b))) & ((p@(ap@(c_2Emeasure_2Esigma__algebra@A_27c)@V4c)) & ((p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27b@A_27c))@V1g)@(ap@(ap@(c_2Epred__set_2EFUNSET@A_27b@A_27c)@(ap@(c_2Emeasure_2Espace@A_27b)@V3b))@(ap@(c_2Emeasure_2Espace@A_27c)@V4c)))) & ((p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27b)@(ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V0f)@(ap@(c_2Emeasure_2Espace@A_27a)@V2a)))@V5t)) & ( ! [V6s:$i] : ((mem@V6s@(arr@A_27c@bool)) => ((p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27c@bool))@V6s)@(ap@(c_2Emeasure_2Esubsets@A_27c)@V4c))) => (p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27b@bool))@(ap@(ap@(c_2Epred__set_2EINTER@A_27b)@(ap@(ap@(c_2Epred__set_2EPREIMAGE@A_27b@A_27c)@V1g)@V6s))@V5t))@(ap@(c_2Emeasure_2Esubsets@A_27b)@V3b)))))))))) => (p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@A_27c))@(ap@(ap@(c_2Ecombin_2Eo@A_27a@A_27c@A_27b)@V1g)@V0f))@(ap@(ap@(c_2Emeasure_2Emeasurable@A_27a@A_27c)@V2a)@V4c)))))))))))))))))))).
thf(conj_thm_2Emeasure_2EMEASURABLE__UP__LIFT,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0sp:$i] : ((mem@V0sp@(arr@A_27a@bool)) => ( ! [V1a:$i] : ((mem@V1a@(arr@(arr@A_27a@bool)@bool)) => ( ! [V2b:$i] : ((mem@V2b@(arr@(arr@A_27a@bool)@bool)) => ( ! [V3c:$i] : ((mem@V3c@(ty_2Epair_2Eprod@(arr@A_27b@bool)@(arr@(arr@A_27b@bool)@bool))) => ( ! [V4f:$i] : ((mem@V4f@(arr@A_27a@A_27b)) => (((p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@A_27b))@V4f)@(ap@(ap@(c_2Emeasure_2Emeasurable@A_27a@A_27b)@(ap@(ap@(c_2Epair_2E_2C@(arr@A_27a@bool)@(arr@(arr@A_27a@bool)@bool))@V0sp)@V1a))@V3c))) & ((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)@V2b))) & (p@(ap@(ap@(c_2Epred__set_2ESUBSET@(arr@A_27a@bool))@V1a)@V2b)))) => (p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@A_27b))@V4f)@(ap@(ap@(c_2Emeasure_2Emeasurable@A_27a@A_27b)@(ap@(ap@(c_2Epair_2E_2C@(arr@A_27a@bool)@(arr@(arr@A_27a@bool)@bool))@V0sp)@V2b))@V3c))))))))))))))))).
thf(conj_thm_2Emeasure_2EMEASURABLE__UP__SUBSET,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0sp:$i] : ((mem@V0sp@(arr@A_27a@bool)) => ( ! [V1a:$i] : ((mem@V1a@(arr@(arr@A_27a@bool)@bool)) => ( ! [V2b:$i] : ((mem@V2b@(arr@(arr@A_27a@bool)@bool)) => ( ! [V3c:$i] : ((mem@V3c@(ty_2Epair_2Eprod@(arr@A_27b@bool)@(arr@(arr@A_27b@bool)@bool))) => (((p@(ap@(ap@(c_2Epred__set_2ESUBSET@(arr@A_27a@bool))@V1a)@V2b)) & (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)@V2b)))) => (p@(ap@(ap@(c_2Epred__set_2ESUBSET@(arr@A_27a@A_27b))@(ap@(ap@(c_2Emeasure_2Emeasurable@A_27a@A_27b)@(ap@(ap@(c_2Epair_2E_2C@(arr@A_27a@bool)@(arr@(arr@A_27a@bool)@bool))@V0sp)@V1a))@V3c))@(ap@(ap@(c_2Emeasure_2Emeasurable@A_27a@A_27b)@(ap@(ap@(c_2Epair_2E_2C@(arr@A_27a@bool)@(arr@(arr@A_27a@bool)@bool))@V0sp)@V2b))@V3c))))))))))))))).
thf(conj_thm_2Emeasure_2EMEASURABLE__UP__SIGMA,lemma,( ! [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))) => (p@(ap@(ap@(c_2Epred__set_2ESUBSET@(arr@A_27a@A_27b))@(ap@(ap@(c_2Emeasure_2Emeasurable@A_27a@A_27b)@V0a)@V1b))@(ap@(ap@(c_2Emeasure_2Emeasurable@A_27a@A_27b)@(ap@(ap@(c_2Emeasure_2Esigma@A_27a)@(ap@(c_2Emeasure_2Espace@A_27a)@V0a))@(ap@(c_2Emeasure_2Esubsets@A_27a)@V0a)))@V1b)))))))))).
thf(conj_thm_2Emeasure_2EMEASURE__PRESERVING__UP__LIFT,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0a:$i] : ((mem@V0a@(arr@(arr@A_27a@bool)@bool)) => ( ! [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)))) => ( ! [V2m2:$i] : ((mem@V2m2@(ty_2Epair_2Eprod@(arr@A_27b@bool)@(ty_2Epair_2Eprod@(arr@(arr@A_27b@bool)@bool)@(arr@(arr@A_27b@bool)@ty_2Erealax_2Ereal)))) => ( ! [V3f:$i] : ((mem@V3f@(arr@A_27a@A_27b)) => (((p@(ap@(c_2Emeasure_2Emeasure__space@A_27a)@V1m1)) & ((p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@A_27b))@V3f)@(ap@(ap@(c_2Emeasure_2Emeasure__preserving@A_27a@A_27b)@(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)@V1m1))@(ap@(ap@(c_2Epair_2E_2C@(arr@(arr@A_27a@bool)@bool)@(arr@(arr@A_27a@bool)@ty_2Erealax_2Ereal))@V0a)@(ap@(c_2Emeasure_2Emeasure@A_27a)@V1m1))))@V2m2))) & ((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)@V1m1))@(ap@(c_2Emeasure_2Emeasurable__sets@A_27a)@V1m1)))) & (p@(ap@(ap@(c_2Epred__set_2ESUBSET@(arr@A_27a@bool))@V0a)@(ap@(c_2Emeasure_2Emeasurable__sets@A_27a)@V1m1)))))) => (p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@A_27b))@V3f)@(ap@(ap@(c_2Emeasure_2Emeasure__preserving@A_27a@A_27b)@V1m1)@V2m2))))))))))))))).
thf(conj_thm_2Emeasure_2EMEASURE__PRESERVING__UP__SUBSET,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0a:$i] : ((mem@V0a@(arr@(arr@A_27a@bool)@bool)) => ( ! [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)))) => ( ! [V2m2:$i] : ((mem@V2m2@(ty_2Epair_2Eprod@(arr@A_27b@bool)@(ty_2Epair_2Eprod@(arr@(arr@A_27b@bool)@bool)@(arr@(arr@A_27b@bool)@ty_2Erealax_2Ereal)))) => (((p@(ap@(c_2Emeasure_2Emeasure__space@A_27a)@V1m1)) & ((p@(ap@(ap@(c_2Epred__set_2ESUBSET@(arr@A_27a@bool))@V0a)@(ap@(c_2Emeasure_2Emeasurable__sets@A_27a)@V1m1))) & (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)@V1m1))@(ap@(c_2Emeasure_2Emeasurable__sets@A_27a)@V1m1)))))) => (p@(ap@(ap@(c_2Epred__set_2ESUBSET@(arr@A_27a@A_27b))@(ap@(ap@(c_2Emeasure_2Emeasure__preserving@A_27a@A_27b)@(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)@V1m1))@(ap@(ap@(c_2Epair_2E_2C@(arr@(arr@A_27a@bool)@bool)@(arr@(arr@A_27a@bool)@ty_2Erealax_2Ereal))@V0a)@(ap@(c_2Emeasure_2Emeasure@A_27a)@V1m1))))@V2m2))@(ap@(ap@(c_2Emeasure_2Emeasure__preserving@A_27a@A_27b)@V1m1)@V2m2))))))))))))).
thf(conj_thm_2Emeasure_2EMEASURE__PRESERVING__UP__SIGMA,lemma,( ! [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)))) => ( ! [V2a:$i] : ((mem@V2a@(arr@(arr@A_27a@bool)@bool)) => (((p@(ap@(c_2Emeasure_2Emeasure__space@A_27a)@V0m1)) & ((ap@(c_2Emeasure_2Emeasurable__sets@A_27a)@V0m1) = (ap@(c_2Emeasure_2Esubsets@A_27a)@(ap@(ap@(c_2Emeasure_2Esigma@A_27a)@(ap@(c_2Emeasure_2Em__space@A_27a)@V0m1))@V2a)))) => (p@(ap@(ap@(c_2Epred__set_2ESUBSET@(arr@A_27a@A_27b))@(ap@(ap@(c_2Emeasure_2Emeasure__preserving@A_27a@A_27b)@(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)@V0m1))@(ap@(ap@(c_2Epair_2E_2C@(arr@(arr@A_27a@bool)@bool)@(arr@(arr@A_27a@bool)@ty_2Erealax_2Ereal))@V2a)@(ap@(c_2Emeasure_2Emeasure@A_27a)@V0m1))))@V1m2))@(ap@(ap@(c_2Emeasure_2Emeasure__preserving@A_27a@A_27b)@V0m1)@V1m2))))))))))))).
thf(conj_thm_2Emeasure_2EMEASURABLE__PROD__SIGMA,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0a:$i] : ((mem@V0a@(ty_2Epair_2Eprod@(arr@A_27a@bool)@(arr@(arr@A_27a@bool)@bool))) => ( ! [V1a1:$i] : ((mem@V1a1@(ty_2Epair_2Eprod@(arr@A_27b@bool)@(arr@(arr@A_27b@bool)@bool))) => ( ! [V2a2:$i] : ((mem@V2a2@(ty_2Epair_2Eprod@(arr@A_27c@bool)@(arr@(arr@A_27c@bool)@bool))) => ( ! [V3f:$i] : ((mem@V3f@(arr@A_27a@(ty_2Epair_2Eprod@A_27b@A_27c))) => (((p@(ap@(c_2Emeasure_2Esigma__algebra@A_27a)@V0a)) & ((p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@A_27b))@(ap@(ap@(c_2Ecombin_2Eo@A_27a@A_27b@(ty_2Epair_2Eprod@A_27b@A_27c))@(c_2Epair_2EFST@A_27b@A_27c))@V3f))@(ap@(ap@(c_2Emeasure_2Emeasurable@A_27a@A_27b)@V0a)@V1a1))) & (p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@A_27c))@(ap@(ap@(c_2Ecombin_2Eo@A_27a@A_27c@(ty_2Epair_2Eprod@A_27b@A_27c))@(c_2Epair_2ESND@A_27b@A_27c))@V3f))@(ap@(ap@(c_2Emeasure_2Emeasurable@A_27a@A_27c)@V0a)@V2a2))))) => (p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@(ty_2Epair_2Eprod@A_27b@A_27c)))@V3f)@(ap@(ap@(c_2Emeasure_2Emeasurable@A_27a@(ty_2Epair_2Eprod@A_27b@A_27c))@V0a)@(ap@(ap@(c_2Emeasure_2Esigma@(ty_2Epair_2Eprod@A_27b@A_27c))@(ap@(ap@(c_2Epred__set_2ECROSS@A_27b@A_27c)@(ap@(c_2Emeasure_2Espace@A_27b)@V1a1))@(ap@(c_2Emeasure_2Espace@A_27c)@V2a2)))@(ap@(ap@(c_2Eutil__prob_2Eprod__sets@A_27b@A_27c)@(ap@(c_2Emeasure_2Esubsets@A_27b)@V1a1))@(ap@(c_2Emeasure_2Esubsets@A_27c)@V2a2))))))))))))))))))).
thf(conj_thm_2Emeasure_2EMEASURABLE__RANGE__REDUCE,lemma,( ! [A_27a:del]: ( ! [A_27b: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@A_27b)) => ( ! [V2s:$i] : ((mem@V2s@(arr@A_27b@bool)) => (((p@(ap@(c_2Emeasure_2Emeasure__space@A_27a)@V0m)) & ((p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@A_27b))@V1f)@(ap@(ap@(c_2Emeasure_2Emeasurable@A_27a@A_27b)@(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)))@(ap@(ap@(c_2Epair_2E_2C@(arr@A_27b@bool)@(arr@(arr@A_27b@bool)@bool))@V2s)@(ap@(c_2Epred__set_2EPOW@A_27b)@V2s))))) & (~~ (V2s = (c_2Epred__set_2EEMPTY@A_27b))))) => (p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@A_27b))@V1f)@(ap@(ap@(c_2Emeasure_2Emeasurable@A_27a@A_27b)@(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)))@(ap@(ap@(c_2Epair_2E_2C@(arr@A_27b@bool)@(arr@(arr@A_27b@bool)@bool))@(ap@(ap@(c_2Epred__set_2EINTER@A_27b)@V2s)@(ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V1f)@(ap@(c_2Emeasure_2Em__space@A_27a)@V0m))))@(ap@(c_2Epred__set_2EPOW@A_27b)@(ap@(ap@(c_2Epred__set_2EINTER@A_27b)@V2s)@(ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V1f)@(ap@(c_2Emeasure_2Em__space@A_27a)@V0m)))))))))))))))))).
thf(conj_thm_2Emeasure_2EMEASURABLE__POW__TO__POW,lemma,( ! [A_27a:del]: ( ! [A_27b: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@A_27b)) => (((p@(ap@(c_2Emeasure_2Emeasure__space@A_27a)@V0m)) & ((ap@(c_2Emeasure_2Emeasurable__sets@A_27a)@V0m) = (ap@(c_2Epred__set_2EPOW@A_27a)@(ap@(c_2Emeasure_2Em__space@A_27a)@V0m)))) => (p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@A_27b))@V1f)@(ap@(ap@(c_2Emeasure_2Emeasurable@A_27a@A_27b)@(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)))@(ap@(ap@(c_2Epair_2E_2C@(arr@A_27b@bool)@(arr@(arr@A_27b@bool)@bool))@(c_2Epred__set_2EUNIV@A_27b))@(ap@(c_2Epred__set_2EPOW@A_27b)@(c_2Epred__set_2EUNIV@A_27b)))))))))))))).
thf(conj_thm_2Emeasure_2EMEASURABLE__POW__TO__POW__IMAGE,lemma,( ! [A_27a:del]: ( ! [A_27b: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@A_27b)) => (((p@(ap@(c_2Emeasure_2Emeasure__space@A_27a)@V0m)) & ((ap@(c_2Emeasure_2Emeasurable__sets@A_27a)@V0m) = (ap@(c_2Epred__set_2EPOW@A_27a)@(ap@(c_2Emeasure_2Em__space@A_27a)@V0m)))) => (p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@A_27b))@V1f)@(ap@(ap@(c_2Emeasure_2Emeasurable@A_27a@A_27b)@(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)))@(ap@(ap@(c_2Epair_2E_2C@(arr@A_27b@bool)@(arr@(arr@A_27b@bool)@bool))@(ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V1f)@(ap@(c_2Emeasure_2Em__space@A_27a)@V0m)))@(ap@(c_2Epred__set_2EPOW@A_27b)@(ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V1f)@(ap@(c_2Emeasure_2Em__space@A_27a)@V0m))))))))))))))).
thf(conj_thm_2Emeasure_2EMEASURE__SPACE__SUBSET,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1s_27:$i] : ((mem@V1s_27@(arr@A_27a@bool)) => ( ! [V2m:$i] : ((mem@V2m@(arr@(arr@A_27a@bool)@ty_2Erealax_2Ereal)) => (((p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V1s_27)@V0s)) & (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)))@V0s)@(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)@V0s))@V2m))))) => (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)))@V1s_27)@(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)@V1s_27))@V2m))))))))))))).
thf(conj_thm_2Emeasure_2ESTRONG__MEASURE__SPACE__SUBSET,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(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_27:$i] : ((mem@V1s_27@(arr@A_27a@bool)) => (((p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V1s_27)@(ap@(c_2Emeasure_2Em__space@A_27a)@V0s))) & ((p@(ap@(c_2Emeasure_2Emeasure__space@A_27a)@V0s)) & (p@(ap@(ap@(c_2Epred__set_2ESUBSET@(arr@A_27a@bool))@(ap@(c_2Epred__set_2EPOW@A_27a)@V1s_27))@(ap@(c_2Emeasure_2Emeasurable__sets@A_27a)@V0s))))) => (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)))@V1s_27)@(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)@V1s_27))@(ap@(c_2Emeasure_2Emeasure@A_27a)@V0s)))))))))))).
thf(conj_thm_2Emeasure_2EMEASURE__REAL__SUM__IMAGE,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))) & (( ! [V2x:$i] : ((mem@V2x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V1s)) => (p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@bool))@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V2x)@(c_2Epred__set_2EEMPTY@A_27a)))@(ap@(c_2Emeasure_2Emeasurable__sets@A_27a)@V0m)))))) & (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V1s))))) => ((surj__ty_2Erealax_2Ereal @ (ap@(ap@(c_2Emeasure_2Emeasure@A_27a)@V0m)@V1s)) = (surj__ty_2Erealax_2Ereal @ (ap@(ap@(c_2Ereal__sigma_2EREAL__SUM__IMAGE@A_27a)@(lam@A_27a@(^ [V3x:$i] : (ap@(ap@(c_2Emeasure_2Emeasure@A_27a)@V0m)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V3x)@(c_2Epred__set_2EEMPTY@A_27a))))))@V1s)))))))))).
thf(conj_thm_2Emeasure_2ESIGMA__POW,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((ap@(ap@(c_2Emeasure_2Esigma@A_27a)@V0s)@(ap@(c_2Epred__set_2EPOW@A_27a)@V0s)) = (ap@(ap@(c_2Epair_2E_2C@(arr@A_27a@bool)@(arr@(arr@A_27a@bool)@bool))@V0s)@(ap@(c_2Epred__set_2EPOW@A_27a)@V0s))))))).
thf(conj_thm_2Emeasure_2Efinite__additivity__sufficient__for__finite__spaces,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(ty_2Epair_2Eprod@(arr@A_27a@bool)@(arr@(arr@A_27a@bool)@bool))) => ( ! [V1m:$i] : ((mem@V1m@(arr@(arr@A_27a@bool)@ty_2Erealax_2Ereal)) => (((p@(ap@(c_2Emeasure_2Esigma__algebra@A_27a)@V0s)) & ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@(ap@(c_2Emeasure_2Espace@A_27a)@V0s))) & ((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)@V0s))@(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)@V0s))@V1m)))) & (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)@V0s))@(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)@V0s))@V1m))))))) => (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)@V0s))@(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)@V0s))@V1m))))))))))).
thf(conj_thm_2Emeasure_2Efinite__additivity__sufficient__for__finite__spaces2,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_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_2Epred__set_2EFINITE@A_27a)@(ap@(c_2Emeasure_2Em__space@A_27a)@V0m))) & ((p@(ap@(c_2Emeasure_2Epositive@A_27a)@V0m)) & (p@(ap@(c_2Emeasure_2Eadditive@A_27a)@V0m))))) => (p@(ap@(c_2Emeasure_2Emeasure__space@A_27a)@V0m))))))).
thf(conj_thm_2Emeasure_2EIMAGE__SING,conjecture,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1x:$i] : ((mem@V1x@A_27a) => ((ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V0f)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V1x)@(c_2Epred__set_2EEMPTY@A_27a))) = (ap@(ap@(c_2Epred__set_2EINSERT@A_27b)@(ap@V0f@V1x))@(c_2Epred__set_2EEMPTY@A_27b)))))))))).
