include('Axioms/HL4001^2.ax').
thf(tp_c_2Emin_2E_40,type,(c_2Emin_2E_40:(del>$i))).
thf(mem_c_2Emin_2E_40,axiom,( ! [A_27a:del] : (mem@(c_2Emin_2E_40@A_27a)@(arr@(arr@A_27a@bool)@A_27a)))).
thf(tp_c_2Ecombin_2EI,type,(c_2Ecombin_2EI:(del>$i))).
thf(mem_c_2Ecombin_2EI,axiom,( ! [A_27a:del] : (mem@(c_2Ecombin_2EI@A_27a)@(arr@A_27a@A_27a)))).
thf(tp_c_2Ecombin_2Eo,type,(c_2Ecombin_2Eo:(del>(del>(del>$i))))).
thf(mem_c_2Ecombin_2Eo,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : ( ! [A_27c:del] : (mem@(c_2Ecombin_2Eo@A_27a@A_27b@A_27c)@(arr@(arr@A_27c@A_27b)@(arr@(arr@A_27a@A_27c)@(arr@A_27a@A_27b)))))))).
thf(tp_ty_2Erealax_2Ereal,type,( ty_2Erealax_2Ereal:del )).
thf(stp_ty_2Erealax_2Ereal,type,(tp__ty_2Erealax_2Ereal : $tType)).
thf(stp_inj_ty_2Erealax_2Ereal,type,(inj__ty_2Erealax_2Ereal : (tp__ty_2Erealax_2Ereal > $i))).
thf(stp_surj_ty_2Erealax_2Ereal,type,(surj__ty_2Erealax_2Ereal : ($i > tp__ty_2Erealax_2Ereal))).
thf(stp_inj_surj_ty_2Erealax_2Ereal,axiom,( ! [X:tp__ty_2Erealax_2Ereal] : ((surj__ty_2Erealax_2Ereal @ (inj__ty_2Erealax_2Ereal @ X)) = X))).
thf(stp_inj_mem_ty_2Erealax_2Ereal,axiom,( ! [X:tp__ty_2Erealax_2Ereal] : (mem @ (inj__ty_2Erealax_2Ereal @ X) @ ty_2Erealax_2Ereal))).
thf(stp_iso_mem_ty_2Erealax_2Ereal,axiom,( ! [X:$i] : ((mem @ X @ ty_2Erealax_2Ereal) => (X = (inj__ty_2Erealax_2Ereal @ (surj__ty_2Erealax_2Ereal @ X)))))).
thf(tp_c_2Erealax_2Ereal__lt,type,(c_2Erealax_2Ereal__lt:$i)).
thf(mem_c_2Erealax_2Ereal__lt,axiom,(mem@c_2Erealax_2Ereal__lt@(arr@ty_2Erealax_2Ereal@(arr@ty_2Erealax_2Ereal@bool)))).
thf(tp_c_2Ebool_2ECOND,type,(c_2Ebool_2ECOND:(del>$i))).
thf(mem_c_2Ebool_2ECOND,axiom,( ! [A_27a:del] : (mem@(c_2Ebool_2ECOND@A_27a)@(arr@bool@(arr@A_27a@(arr@A_27a@A_27a)))))).
thf(tp_ty_2Eextreal_2Eextreal,type,( ty_2Eextreal_2Eextreal:del )).
thf(stp_ty_2Eextreal_2Eextreal,type,(tp__ty_2Eextreal_2Eextreal : $tType)).
thf(stp_inj_ty_2Eextreal_2Eextreal,type,(inj__ty_2Eextreal_2Eextreal : (tp__ty_2Eextreal_2Eextreal > $i))).
thf(stp_surj_ty_2Eextreal_2Eextreal,type,(surj__ty_2Eextreal_2Eextreal : ($i > tp__ty_2Eextreal_2Eextreal))).
thf(stp_inj_surj_ty_2Eextreal_2Eextreal,axiom,( ! [X:tp__ty_2Eextreal_2Eextreal] : ((surj__ty_2Eextreal_2Eextreal @ (inj__ty_2Eextreal_2Eextreal @ X)) = X))).
thf(stp_inj_mem_ty_2Eextreal_2Eextreal,axiom,( ! [X:tp__ty_2Eextreal_2Eextreal] : (mem @ (inj__ty_2Eextreal_2Eextreal @ X) @ ty_2Eextreal_2Eextreal))).
thf(stp_iso_mem_ty_2Eextreal_2Eextreal,axiom,( ! [X:$i] : ((mem @ X @ ty_2Eextreal_2Eextreal) => (X = (inj__ty_2Eextreal_2Eextreal @ (surj__ty_2Eextreal_2Eextreal @ X)))))).
thf(tp_c_2Eextreal_2Ereal,type,(c_2Eextreal_2Ereal:$i)).
thf(mem_c_2Eextreal_2Ereal,axiom,(mem@c_2Eextreal_2Ereal@(arr@ty_2Eextreal_2Eextreal@ty_2Erealax_2Ereal))).
thf(stp_fo_c_2Eextreal_2Ereal,type,(fo__c_2Eextreal_2Ereal:(tp__ty_2Eextreal_2Eextreal > tp__ty_2Erealax_2Ereal))).
thf(stp_eq_fo_c_2Eextreal_2Ereal,axiom,( ! [X0:tp__ty_2Eextreal_2Eextreal] : ((inj__ty_2Erealax_2Ereal @ (fo__c_2Eextreal_2Ereal @ X0)) = (ap @ c_2Eextreal_2Ereal @ (inj__ty_2Eextreal_2Eextreal @ X0))))).
thf(tp_ty_2Epair_2Eprod,type,( ty_2Epair_2Eprod: del > del >del )).
thf(tp_c_2Elebesgue_2Eprod__measure__space,type,(c_2Elebesgue_2Eprod__measure__space:(del>(del>$i)))).
thf(mem_c_2Elebesgue_2Eprod__measure__space,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Elebesgue_2Eprod__measure__space@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)))@(ty_2Epair_2Eprod@(arr@(ty_2Epair_2Eprod@A_27a@A_27b)@bool)@(ty_2Epair_2Eprod@(arr@(arr@(ty_2Epair_2Eprod@A_27a@A_27b)@bool)@bool)@(arr@(arr@(ty_2Epair_2Eprod@A_27a@A_27b)@bool)@ty_2Erealax_2Ereal))))))))).
thf(tp_c_2Eextreal_2ENormal,type,(c_2Eextreal_2ENormal:$i)).
thf(mem_c_2Eextreal_2ENormal,axiom,(mem@c_2Eextreal_2ENormal@(arr@ty_2Erealax_2Ereal@ty_2Eextreal_2Eextreal))).
thf(stp_fo_c_2Eextreal_2ENormal,type,(fo__c_2Eextreal_2ENormal:(tp__ty_2Erealax_2Ereal > tp__ty_2Eextreal_2Eextreal))).
thf(stp_eq_fo_c_2Eextreal_2ENormal,axiom,( ! [X0:tp__ty_2Erealax_2Ereal] : ((inj__ty_2Eextreal_2Eextreal @ (fo__c_2Eextreal_2ENormal @ X0)) = (ap @ c_2Eextreal_2ENormal @ (inj__ty_2Erealax_2Ereal @ X0))))).
thf(tp_c_2Eextreal_2Eextreal__mul,type,(c_2Eextreal_2Eextreal__mul:$i)).
thf(mem_c_2Eextreal_2Eextreal__mul,axiom,(mem@c_2Eextreal_2Eextreal__mul@(arr@ty_2Eextreal_2Eextreal@(arr@ty_2Eextreal_2Eextreal@ty_2Eextreal_2Eextreal)))).
thf(stp_fo_c_2Eextreal_2Eextreal__mul,type,(fo__c_2Eextreal_2Eextreal__mul:(tp__ty_2Eextreal_2Eextreal > (tp__ty_2Eextreal_2Eextreal > tp__ty_2Eextreal_2Eextreal)))).
thf(stp_eq_fo_c_2Eextreal_2Eextreal__mul,axiom,( ! [X0:tp__ty_2Eextreal_2Eextreal] : ( ! [X1:tp__ty_2Eextreal_2Eextreal] : ((inj__ty_2Eextreal_2Eextreal @ ((fo__c_2Eextreal_2Eextreal__mul @ X0) @ X1)) = (ap @ (ap @ c_2Eextreal_2Eextreal__mul @ (inj__ty_2Eextreal_2Eextreal @ X0)) @ (inj__ty_2Eextreal_2Eextreal @ X1)))))).
thf(tp_c_2Eextreal_2EEXTREAL__SUM__IMAGE,type,(c_2Eextreal_2EEXTREAL__SUM__IMAGE:(del>$i))).
thf(mem_c_2Eextreal_2EEXTREAL__SUM__IMAGE,axiom,( ! [A_27a:del] : (mem@(c_2Eextreal_2EEXTREAL__SUM__IMAGE@A_27a)@(arr@(arr@A_27a@ty_2Eextreal_2Eextreal)@(arr@(arr@A_27a@bool)@ty_2Eextreal_2Eextreal))))).
thf(tp_c_2Elebesgue_2Eintegral,type,(c_2Elebesgue_2Eintegral:(del>$i))).
thf(mem_c_2Elebesgue_2Eintegral,axiom,( ! [A_27a:del] : (mem@(c_2Elebesgue_2Eintegral@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)@ty_2Eextreal_2Eextreal))))).
thf(tp_c_2Eextreal_2EPosInf,type,(c_2Eextreal_2EPosInf:$i)).
thf(mem_c_2Eextreal_2EPosInf,axiom,(mem@c_2Eextreal_2EPosInf@ty_2Eextreal_2Eextreal)).
thf(stp_fo_c_2Eextreal_2EPosInf,type,(fo__c_2Eextreal_2EPosInf:tp__ty_2Eextreal_2Eextreal)).
thf(stp_eq_fo_c_2Eextreal_2EPosInf,axiom,((inj__ty_2Eextreal_2Eextreal @ fo__c_2Eextreal_2EPosInf) = c_2Eextreal_2EPosInf)).
thf(tp_c_2Eextreal_2ENegInf,type,(c_2Eextreal_2ENegInf:$i)).
thf(mem_c_2Eextreal_2ENegInf,axiom,(mem@c_2Eextreal_2ENegInf@ty_2Eextreal_2Eextreal)).
thf(stp_fo_c_2Eextreal_2ENegInf,type,(fo__c_2Eextreal_2ENegInf:tp__ty_2Eextreal_2Eextreal)).
thf(stp_eq_fo_c_2Eextreal_2ENegInf,axiom,((inj__ty_2Eextreal_2Eextreal @ fo__c_2Eextreal_2ENegInf) = c_2Eextreal_2ENegInf)).
thf(tp_c_2Elebesgue_2Eprod__measure,type,(c_2Elebesgue_2Eprod__measure:(del>(del>$i)))).
thf(mem_c_2Elebesgue_2Eprod__measure,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Elebesgue_2Eprod__measure@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@(ty_2Epair_2Eprod@A_27a@A_27b)@bool)@ty_2Erealax_2Ereal))))))).
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_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_2Epred__set_2EBIGUNION,type,(c_2Epred__set_2EBIGUNION:(del>$i))).
thf(mem_c_2Epred__set_2EBIGUNION,axiom,( ! [A_27a:del] : (mem@(c_2Epred__set_2EBIGUNION@A_27a)@(arr@(arr@(arr@A_27a@bool)@bool)@(arr@A_27a@bool))))).
thf(tp_c_2Epred__set_2Ecountable,type,(c_2Epred__set_2Ecountable:(del>$i))).
thf(mem_c_2Epred__set_2Ecountable,axiom,( ! [A_27a:del] : (mem@(c_2Epred__set_2Ecountable@A_27a)@(arr@(arr@A_27a@bool)@bool)))).
thf(tp_c_2Epred__set_2EDIFF,type,(c_2Epred__set_2EDIFF:(del>$i))).
thf(mem_c_2Epred__set_2EDIFF,axiom,( ! [A_27a:del] : (mem@(c_2Epred__set_2EDIFF@A_27a)@(arr@(arr@A_27a@bool)@(arr@(arr@A_27a@bool)@(arr@A_27a@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_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_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_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__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__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_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_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(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_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_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_2Ebool_2ET,type,(c_2Ebool_2ET:$i)).
thf(mem_c_2Ebool_2ET,axiom,(mem@c_2Ebool_2ET@bool)).
thf(ax_true_p,axiom,(p@c_2Ebool_2ET)).
thf(tp_c_2Epred__set_2EUNION,type,(c_2Epred__set_2EUNION:(del>$i))).
thf(mem_c_2Epred__set_2EUNION,axiom,( ! [A_27a:del] : (mem@(c_2Epred__set_2EUNION@A_27a)@(arr@(arr@A_27a@bool)@(arr@(arr@A_27a@bool)@(arr@A_27a@bool)))))).
thf(tp_c_2Epred__set_2EINTER,type,(c_2Epred__set_2EINTER:(del>$i))).
thf(mem_c_2Epred__set_2EINTER,axiom,( ! [A_27a:del] : (mem@(c_2Epred__set_2EINTER@A_27a)@(arr@(arr@A_27a@bool)@(arr@(arr@A_27a@bool)@(arr@A_27a@bool)))))).
thf(tp_c_2Ebool_2E_3F,type,(c_2Ebool_2E_3F:(del>$i))).
thf(mem_c_2Ebool_2E_3F,axiom,( ! [A_27a:del] : (mem@(c_2Ebool_2E_3F@A_27a)@(arr@(arr@A_27a@bool)@bool)))).
thf(ax_ex_p,axiom,( ! [A:del] : ( ! [Q:$i] : ((mem@Q@(arr@A@bool)) => ((p@(ap@(c_2Ebool_2E_3F@A)@Q)) <=> (? [X:$i] : ((mem@X@A) & (p@(ap@Q@X))))))))).
thf(tp_c_2Epred__set_2EDISJOINT,type,(c_2Epred__set_2EDISJOINT:(del>$i))).
thf(mem_c_2Epred__set_2EDISJOINT,axiom,( ! [A_27a:del] : (mem@(c_2Epred__set_2EDISJOINT@A_27a)@(arr@(arr@A_27a@bool)@(arr@(arr@A_27a@bool)@bool))))).
thf(tp_c_2Epred__set_2EINSERT,type,(c_2Epred__set_2EINSERT:(del>$i))).
thf(mem_c_2Epred__set_2EINSERT,axiom,( ! [A_27a:del] : (mem@(c_2Epred__set_2EINSERT@A_27a)@(arr@A_27a@(arr@(arr@A_27a@bool)@(arr@A_27a@bool)))))).
thf(tp_c_2Epred__set_2EBIGINTER,type,(c_2Epred__set_2EBIGINTER:(del>$i))).
thf(mem_c_2Epred__set_2EBIGINTER,axiom,( ! [A_27a:del] : (mem@(c_2Epred__set_2EBIGINTER@A_27a)@(arr@(arr@(arr@A_27a@bool)@bool)@(arr@A_27a@bool))))).
thf(tp_c_2Epair_2ESND,type,(c_2Epair_2ESND:(del>(del>$i)))).
thf(mem_c_2Epair_2ESND,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Epair_2ESND@A_27a@A_27b)@(arr@(ty_2Epair_2Eprod@A_27a@A_27b)@A_27b))))).
thf(tp_c_2Epair_2EFST,type,(c_2Epair_2EFST:(del>(del>$i)))).
thf(mem_c_2Epair_2EFST,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Epair_2EFST@A_27a@A_27b)@(arr@(ty_2Epair_2Eprod@A_27a@A_27b)@A_27a))))).
thf(tp_c_2Epred__set_2EEMPTY,type,(c_2Epred__set_2EEMPTY:(del>$i))).
thf(mem_c_2Epred__set_2EEMPTY,axiom,( ! [A_27a:del] : (mem@(c_2Epred__set_2EEMPTY@A_27a)@(arr@A_27a@bool)))).
thf(tp_c_2Epred__set_2ESUBSET,type,(c_2Epred__set_2ESUBSET:(del>$i))).
thf(mem_c_2Epred__set_2ESUBSET,axiom,( ! [A_27a:del] : (mem@(c_2Epred__set_2ESUBSET@A_27a)@(arr@(arr@A_27a@bool)@(arr@(arr@A_27a@bool)@bool))))).
thf(tp_c_2Epred__set_2EPOW,type,(c_2Epred__set_2EPOW:(del>$i))).
thf(mem_c_2Epred__set_2EPOW,axiom,( ! [A_27a:del] : (mem@(c_2Epred__set_2EPOW@A_27a)@(arr@(arr@A_27a@bool)@(arr@(arr@A_27a@bool)@bool))))).
thf(tp_c_2Epred__set_2EPREIMAGE,type,(c_2Epred__set_2EPREIMAGE:(del>(del>$i)))).
thf(mem_c_2Epred__set_2EPREIMAGE,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Epred__set_2EPREIMAGE@A_27a@A_27b)@(arr@(arr@A_27a@A_27b)@(arr@(arr@A_27b@bool)@(arr@A_27a@bool))))))).
thf(tp_c_2Erealax_2Ereal__mul,type,(c_2Erealax_2Ereal__mul:$i)).
thf(mem_c_2Erealax_2Ereal__mul,axiom,(mem@c_2Erealax_2Ereal__mul@(arr@ty_2Erealax_2Ereal@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)))).
thf(stp_fo_c_2Erealax_2Ereal__mul,type,(fo__c_2Erealax_2Ereal__mul:(tp__ty_2Erealax_2Ereal > (tp__ty_2Erealax_2Ereal > tp__ty_2Erealax_2Ereal)))).
thf(stp_eq_fo_c_2Erealax_2Ereal__mul,axiom,( ! [X0:tp__ty_2Erealax_2Ereal] : ( ! [X1:tp__ty_2Erealax_2Ereal] : ((inj__ty_2Erealax_2Ereal @ ((fo__c_2Erealax_2Ereal__mul @ X0) @ X1)) = (ap @ (ap @ c_2Erealax_2Ereal__mul @ (inj__ty_2Erealax_2Ereal @ X0)) @ (inj__ty_2Erealax_2Ereal @ X1)))))).
thf(tp_ty_2Enum_2Enum,type,( ty_2Enum_2Enum:del )).
thf(stp_ty_2Enum_2Enum,type,(tp__ty_2Enum_2Enum : $tType)).
thf(stp_inj_ty_2Enum_2Enum,type,(inj__ty_2Enum_2Enum : (tp__ty_2Enum_2Enum > $i))).
thf(stp_surj_ty_2Enum_2Enum,type,(surj__ty_2Enum_2Enum : ($i > tp__ty_2Enum_2Enum))).
thf(stp_inj_surj_ty_2Enum_2Enum,axiom,( ! [X:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (inj__ty_2Enum_2Enum @ X)) = X))).
thf(stp_inj_mem_ty_2Enum_2Enum,axiom,( ! [X:tp__ty_2Enum_2Enum] : (mem @ (inj__ty_2Enum_2Enum @ X) @ ty_2Enum_2Enum))).
thf(stp_iso_mem_ty_2Enum_2Enum,axiom,( ! [X:$i] : ((mem @ X @ ty_2Enum_2Enum) => (X = (inj__ty_2Enum_2Enum @ (surj__ty_2Enum_2Enum @ X)))))).
thf(tp_c_2Enum_2E0,type,(c_2Enum_2E0:$i)).
thf(mem_c_2Enum_2E0,axiom,(mem@c_2Enum_2E0@ty_2Enum_2Enum)).
thf(stp_fo_c_2Enum_2E0,type,(fo__c_2Enum_2E0:tp__ty_2Enum_2Enum)).
thf(stp_eq_fo_c_2Enum_2E0,axiom,((inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0) = c_2Enum_2E0)).
thf(tp_c_2Ereal_2Ereal__of__num,type,(c_2Ereal_2Ereal__of__num:$i)).
thf(mem_c_2Ereal_2Ereal__of__num,axiom,(mem@c_2Ereal_2Ereal__of__num@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal))).
thf(stp_fo_c_2Ereal_2Ereal__of__num,type,(fo__c_2Ereal_2Ereal__of__num:(tp__ty_2Enum_2Enum > tp__ty_2Erealax_2Ereal))).
thf(stp_eq_fo_c_2Ereal_2Ereal__of__num,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ((inj__ty_2Erealax_2Ereal @ (fo__c_2Ereal_2Ereal__of__num @ X0)) = (ap @ c_2Ereal_2Ereal__of__num @ (inj__ty_2Enum_2Enum @ X0))))).
thf(tp_c_2Ereal_2Ereal__lte,type,(c_2Ereal_2Ereal__lte:$i)).
thf(mem_c_2Ereal_2Ereal__lte,axiom,(mem@c_2Ereal_2Ereal__lte@(arr@ty_2Erealax_2Ereal@(arr@ty_2Erealax_2Ereal@bool)))).
thf(tp_c_2Erealax_2Ereal__add,type,(c_2Erealax_2Ereal__add:$i)).
thf(mem_c_2Erealax_2Ereal__add,axiom,(mem@c_2Erealax_2Ereal__add@(arr@ty_2Erealax_2Ereal@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)))).
thf(stp_fo_c_2Erealax_2Ereal__add,type,(fo__c_2Erealax_2Ereal__add:(tp__ty_2Erealax_2Ereal > (tp__ty_2Erealax_2Ereal > tp__ty_2Erealax_2Ereal)))).
thf(stp_eq_fo_c_2Erealax_2Ereal__add,axiom,( ! [X0:tp__ty_2Erealax_2Ereal] : ( ! [X1:tp__ty_2Erealax_2Ereal] : ((inj__ty_2Erealax_2Ereal @ ((fo__c_2Erealax_2Ereal__add @ X0) @ X1)) = (ap @ (ap @ c_2Erealax_2Ereal__add @ (inj__ty_2Erealax_2Ereal @ X0)) @ (inj__ty_2Erealax_2Ereal @ X1)))))).
thf(tp_c_2Ereal__sigma_2EREAL__SUM__IMAGE,type,(c_2Ereal__sigma_2EREAL__SUM__IMAGE:(del>$i))).
thf(mem_c_2Ereal__sigma_2EREAL__SUM__IMAGE,axiom,( ! [A_27a:del] : (mem@(c_2Ereal__sigma_2EREAL__SUM__IMAGE@A_27a)@(arr@(arr@A_27a@ty_2Erealax_2Ereal)@(arr@(arr@A_27a@bool)@ty_2Erealax_2Ereal))))).
thf(tp_c_2Epred__set_2EFINITE,type,(c_2Epred__set_2EFINITE:(del>$i))).
thf(mem_c_2Epred__set_2EFINITE,axiom,( ! [A_27a:del] : (mem@(c_2Epred__set_2EFINITE@A_27a)@(arr@(arr@A_27a@bool)@bool)))).
thf(tp_c_2Ebool_2EF,type,(c_2Ebool_2EF:$i)).
thf(mem_c_2Ebool_2EF,axiom,(mem@c_2Ebool_2EF@bool)).
thf(ax_false_p,axiom,(~ (p@c_2Ebool_2EF))).
thf(tp_c_2Ebool_2E_5C_2F,type,(c_2Ebool_2E_5C_2F:$i)).
thf(mem_c_2Ebool_2E_5C_2F,axiom,(mem@c_2Ebool_2E_5C_2F@(arr@bool@(arr@bool@bool)))).
thf(ax_or_p,axiom,( ! [Q:$i] : ((mem@Q@bool) => ( ! [R:$i] : ((mem@R@bool) => ((p@(ap@(ap@c_2Ebool_2E_5C_2F@Q)@R)) <=> ((p@Q) | (p@R)))))))).
thf(tp_c_2Ebool_2E_7E,type,(c_2Ebool_2E_7E:$i)).
thf(mem_c_2Ebool_2E_7E,axiom,(mem@c_2Ebool_2E_7E@(arr@bool@bool))).
thf(ax_neg_p,axiom,( ! [Q:$i] : ((mem@Q@bool) => ((p@(ap@c_2Ebool_2E_7E@Q)) <=> (~ (p@Q)))))).
thf(tp_c_2Emin_2E_3D_3D_3E,type,(c_2Emin_2E_3D_3D_3E:$i)).
thf(mem_c_2Emin_2E_3D_3D_3E,axiom,(mem@c_2Emin_2E_3D_3D_3E@(arr@bool@(arr@bool@bool)))).
thf(ax_imp_p,axiom,( ! [Q:$i] : ((mem@Q@bool) => ( ! [R:$i] : ((mem@R@bool) => ((p@(ap@(ap@c_2Emin_2E_3D_3D_3E@Q)@R)) <=> ((p@Q) => (p@R)))))))).
thf(tp_c_2Ebool_2EIN,type,(c_2Ebool_2EIN:(del>$i))).
thf(mem_c_2Ebool_2EIN,axiom,( ! [A_27a:del] : (mem@(c_2Ebool_2EIN@A_27a)@(arr@A_27a@(arr@(arr@A_27a@bool)@bool))))).
thf(tp_c_2Ebool_2E_2F_5C,type,(c_2Ebool_2E_2F_5C:$i)).
thf(mem_c_2Ebool_2E_2F_5C,axiom,(mem@c_2Ebool_2E_2F_5C@(arr@bool@(arr@bool@bool)))).
thf(ax_and_p,axiom,( ! [Q:$i] : ((mem@Q@bool) => ( ! [R:$i] : ((mem@R@bool) => ((p@(ap@(ap@c_2Ebool_2E_2F_5C@Q)@R)) <=> ((p@Q) & (p@R)))))))).
thf(tp_c_2Epred__set_2ECROSS,type,(c_2Epred__set_2ECROSS:(del>(del>$i)))).
thf(mem_c_2Epred__set_2ECROSS,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Epred__set_2ECROSS@A_27a@A_27b)@(arr@(arr@A_27a@bool)@(arr@(arr@A_27b@bool)@(arr@(ty_2Epair_2Eprod@A_27a@A_27b)@bool))))))).
thf(tp_c_2Epair_2E_2C,type,(c_2Epair_2E_2C:(del>(del>$i)))).
thf(mem_c_2Epair_2E_2C,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Epair_2E_2C@A_27a@A_27b)@(arr@A_27a@(arr@A_27b@(ty_2Epair_2Eprod@A_27a@A_27b))))))).
thf(tp_c_2Epair_2EUNCURRY,type,(c_2Epair_2EUNCURRY:(del>(del>(del>$i))))).
thf(mem_c_2Epair_2EUNCURRY,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : ( ! [A_27c:del] : (mem@(c_2Epair_2EUNCURRY@A_27a@A_27b@A_27c)@(arr@(arr@A_27a@(arr@A_27b@A_27c))@(arr@(ty_2Epair_2Eprod@A_27a@A_27b)@A_27c))))))).
thf(tp_c_2Epred__set_2EGSPEC,type,(c_2Epred__set_2EGSPEC:(del>(del>$i)))).
thf(mem_c_2Epred__set_2EGSPEC,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Epred__set_2EGSPEC@A_27a@A_27b)@(arr@(arr@A_27b@(ty_2Epair_2Eprod@A_27a@bool))@(arr@A_27a@bool)))))).
thf(tp_c_2Eutil__prob_2Eprod__sets,type,(c_2Eutil__prob_2Eprod__sets:(del>(del>$i)))).
thf(mem_c_2Eutil__prob_2Eprod__sets,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Eutil__prob_2Eprod__sets@A_27a@A_27b)@(arr@(arr@(arr@A_27a@bool)@bool)@(arr@(arr@(arr@A_27b@bool)@bool)@(arr@(arr@(ty_2Epair_2Eprod@A_27a@A_27b)@bool)@bool))))))).
thf(tp_c_2Emin_2E_3D,type,(c_2Emin_2E_3D:(del>$i))).
thf(mem_c_2Emin_2E_3D,axiom,( ! [A_27a:del] : (mem@(c_2Emin_2E_3D@A_27a)@(arr@A_27a@(arr@A_27a@bool))))).
thf(ax_eq_p,axiom,( ! [A:del] : ( ! [X:$i] : ((mem@X@A) => ( ! [Y:$i] : ((mem@Y@A) => ((p@(ap@(ap@(c_2Emin_2E_3D@A)@X)@Y)) <=> (X = Y)))))))).
thf(tp_c_2Ebool_2E_21,type,(c_2Ebool_2E_21:(del>$i))).
thf(mem_c_2Ebool_2E_21,axiom,( ! [A_27a:del] : (mem@(c_2Ebool_2E_21@A_27a)@(arr@(arr@A_27a@bool)@bool)))).
thf(ax_all_p,axiom,( ! [A:del] : ( ! [Q:$i] : ((mem@Q@(arr@A@bool)) => ((p@(ap@(c_2Ebool_2E_21@A)@Q)) <=> ( ! [X:$i] : ((mem@X@A) => (p@(ap@Q@X))))))))).
thf(ax_thm_2Ebool_2EEXISTS__DEF,axiom,( ! [A_27a:del]: ((c_2Ebool_2E_3F@A_27a) = (lam@(arr@A_27a@bool)@(^ [V0P:$i] : (ap@V0P@(ap@(c_2Emin_2E_40@A_27a)@V0P))))))).
thf(ax_thm_2Ebool_2EETA__AX,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0t:$i] : ((mem@V0t@(arr@A_27a@A_27b)) => ((lam@A_27a@(^ [V1x:$i] : (ap@V0t@V1x))) = V0t)))))).
thf(ax_thm_2Ebool_2ESELECT__AX,axiom,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1x:$i] : ((mem@V1x@A_27a) => ((p@(ap@V0P@V1x)) => (p@(ap@V0P@(ap@(c_2Emin_2E_40@A_27a)@V0P)))))))))).
thf(conj_thm_2Ebool_2ETRUTH,lemma,$true).
thf(conj_thm_2Ebool_2EIMP__ANTISYM__AX,lemma,( ! [V0t1:$i] : ((mem@V0t1@bool) => ( ! [V1t2:$i] : ((mem@V1t2@bool) => (((p@V0t1) => (p@V1t2)) => (((p@V1t2) => (p@V0t1)) => ((p@V0t1) <=> (p@V1t2))))))))).
thf(conj_thm_2Ebool_2EFALSITY,lemma,( ! [V0t:$i] : ((mem@V0t@bool) => ($false => (p@V0t))))).
thf(conj_thm_2Ebool_2EFORALL__SIMP,lemma,( ! [A_27a:del]: ( ! [V0t:$i] : ((mem@V0t@bool) => (( ! [V1x:$i] : ((mem@V1x@A_27a) => (p@V0t))) <=> (p@V0t)))))).
thf(conj_thm_2Ebool_2EAND__CLAUSES,lemma,( ! [V0t:$i] : ((mem@V0t@bool) => ((($true & (p@V0t)) <=> (p@V0t)) & ((((p@V0t) & $true) <=> (p@V0t)) & ((($false & (p@V0t)) <=> $false) & ((((p@V0t) & $false) <=> $false) & (((p@V0t) & (p@V0t)) <=> (p@V0t))))))))).
thf(conj_thm_2Ebool_2EIMP__CLAUSES,lemma,( ! [V0t:$i] : ((mem@V0t@bool) => ((($true => (p@V0t)) <=> (p@V0t)) & ((((p@V0t) => $true) <=> $true) & ((($false => (p@V0t)) <=> $true) & ((((p@V0t) => (p@V0t)) <=> $true) & (((p@V0t) => $false) <=> (~ (p@V0t)))))))))).
thf(conj_thm_2Ebool_2ENOT__CLAUSES,lemma,(( ! [V0t:$i] : ((mem@V0t@bool) => ((~ (~ (p@V0t))) <=> (p@V0t)))) & (((~ ($true)) <=> $false) & ((~ ($false)) <=> $true)))).
thf(conj_thm_2Ebool_2EEQ__REFL,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => (V0x = V0x))))).
thf(conj_thm_2Ebool_2EREFL__CLAUSE,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ((V0x = V0x) <=> $true))))).
thf(conj_thm_2Ebool_2EEQ__SYM__EQ,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1y:$i] : ((mem@V1y@A_27a) => ((V0x = V1y) <=> (V1y = V0x)))))))).
thf(conj_thm_2Ebool_2EEQ__CLAUSES,lemma,( ! [V0t:$i] : ((mem@V0t@bool) => ((($true <=> (p@V0t)) <=> (p@V0t)) & ((((p@V0t) <=> $true) <=> (p@V0t)) & ((($false <=> (p@V0t)) <=> (~ (p@V0t))) & (((p@V0t) <=> $false) <=> (~ (p@V0t))))))))).
thf(conj_thm_2Ebool_2ENOT__EXISTS__THM,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ((~ (? [V1x:$i] : ((mem@V1x@A_27a) & (p@(ap@V0P@V1x))))) <=> ( ! [V2x:$i] : ((mem@V2x@A_27a) => (~ (p@(ap@V0P@V2x)))))))))).
thf(conj_thm_2Ebool_2ELEFT__AND__FORALL__THM,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1Q:$i] : ((mem@V1Q@bool) => ((( ! [V2x:$i] : ((mem@V2x@A_27a) => (p@(ap@V0P@V2x)))) & (p@V1Q)) <=> ( ! [V3x:$i] : ((mem@V3x@A_27a) => ((p@(ap@V0P@V3x)) & (p@V1Q))))))))))).
thf(conj_thm_2Ebool_2ERIGHT__AND__FORALL__THM,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@bool) => ( ! [V1Q:$i] : ((mem@V1Q@(arr@A_27a@bool)) => (((p@V0P) & ( ! [V2x:$i] : ((mem@V2x@A_27a) => (p@(ap@V1Q@V2x))))) <=> ( ! [V3x:$i] : ((mem@V3x@A_27a) => ((p@V0P) & (p@(ap@V1Q@V3x)))))))))))).
thf(conj_thm_2Ebool_2ELEFT__FORALL__OR__THM,lemma,( ! [A_27a:del]: ( ! [V0Q:$i] : ((mem@V0Q@bool) => ( ! [V1P:$i] : ((mem@V1P@(arr@A_27a@bool)) => (( ! [V2x:$i] : ((mem@V2x@A_27a) => ((p@(ap@V1P@V2x)) | (p@V0Q)))) <=> (( ! [V3x:$i] : ((mem@V3x@A_27a) => (p@(ap@V1P@V3x)))) | (p@V0Q))))))))).
thf(conj_thm_2Ebool_2ERIGHT__FORALL__OR__THM,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@bool) => ( ! [V1Q:$i] : ((mem@V1Q@(arr@A_27a@bool)) => (( ! [V2x:$i] : ((mem@V2x@A_27a) => ((p@V0P) | (p@(ap@V1Q@V2x))))) <=> ((p@V0P) | ( ! [V3x:$i] : ((mem@V3x@A_27a) => (p@(ap@V1Q@V3x)))))))))))).
thf(conj_thm_2Ebool_2EDE__MORGAN__THM,lemma,( ! [V0A:$i] : ((mem@V0A@bool) => ( ! [V1B:$i] : ((mem@V1B@bool) => (((~ ((p@V0A) & (p@V1B))) <=> ((~ (p@V0A)) | (~ (p@V1B)))) & ((~ ((p@V0A) | (p@V1B))) <=> ((~ (p@V0A)) & (~ (p@V1B)))))))))).
thf(conj_thm_2Ebool_2ELEFT__OR__OVER__AND,lemma,( ! [V0A:$i] : ((mem@V0A@bool) => ( ! [V1B:$i] : ((mem@V1B@bool) => ( ! [V2C:$i] : ((mem@V2C@bool) => (((p@V0A) | ((p@V1B) & (p@V2C))) <=> (((p@V0A) | (p@V1B)) & ((p@V0A) | (p@V2C))))))))))).
thf(conj_thm_2Ebool_2ERIGHT__OR__OVER__AND,lemma,( ! [V0A:$i] : ((mem@V0A@bool) => ( ! [V1B:$i] : ((mem@V1B@bool) => ( ! [V2C:$i] : ((mem@V2C@bool) => ((((p@V1B) & (p@V2C)) | (p@V0A)) <=> (((p@V1B) | (p@V0A)) & ((p@V2C) | (p@V0A))))))))))).
thf(conj_thm_2Ebool_2EAND__IMP__INTRO,lemma,( ! [V0t1:$i] : ((mem@V0t1@bool) => ( ! [V1t2:$i] : ((mem@V1t2@bool) => ( ! [V2t3:$i] : ((mem@V2t3@bool) => (((p@V0t1) => ((p@V1t2) => (p@V2t3))) <=> (((p@V0t1) & (p@V1t2)) => (p@V2t3)))))))))).
thf(conj_thm_2Ebool_2EIMP__CONG,lemma,( ! [V0x:$i] : ((mem@V0x@bool) => ( ! [V1x_27:$i] : ((mem@V1x_27@bool) => ( ! [V2y:$i] : ((mem@V2y@bool) => ( ! [V3y_27:$i] : ((mem@V3y_27@bool) => ((((p@V0x) <=> (p@V1x_27)) & ((p@V1x_27) => ((p@V2y) <=> (p@V3y_27)))) => (((p@V0x) => (p@V2y)) <=> ((p@V1x_27) => (p@V3y_27))))))))))))).
thf(conj_thm_2Ebool_2EUNWIND__THM2,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1a:$i] : ((mem@V1a@A_27a) => ((? [V2x:$i] : ((mem@V2x@A_27a) & ((V2x = V1a) & (p@(ap@V0P@V2x))))) <=> (p@(ap@V0P@V1a))))))))).
thf(ax_thm_2Ecombin_2Eo__DEF,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27c@A_27b)) => ( ! [V1g:$i] : ((mem@V1g@(arr@A_27a@A_27c)) => ((ap@(ap@(c_2Ecombin_2Eo@A_27a@A_27b@A_27c)@V0f)@V1g) = (lam@A_27a@(^ [V2x:$i] : (ap@V0f@(ap@V1g@V2x))))))))))))).
thf(conj_thm_2Ecombin_2EI__THM,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ((ap@(c_2Ecombin_2EI@A_27a)@V0x) = V0x))))).
thf(conj_thm_2Ecombin_2EI__o__ID,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => (((ap@(ap@(c_2Ecombin_2Eo@A_27a@A_27b@A_27b)@(c_2Ecombin_2EI@A_27b))@V0f) = V0f) & ((ap@(ap@(c_2Ecombin_2Eo@A_27a@A_27b@A_27a)@V0f)@(c_2Ecombin_2EI@A_27a)) = V0f))))))).
thf(conj_thm_2Eextreal_2Ereal__normal,lemma,( ! [V0x:tp__ty_2Erealax_2Ereal] : ((surj__ty_2Erealax_2Ereal @ (ap@c_2Eextreal_2Ereal@(ap@c_2Eextreal_2ENormal@(inj__ty_2Erealax_2Ereal @ V0x)))) = V0x))).
thf(conj_thm_2Eextreal_2Eextreal__mul__def,lemma,( ! [V0x:tp__ty_2Erealax_2Ereal] : ( ! [V1y:tp__ty_2Erealax_2Ereal] : (((surj__ty_2Eextreal_2Eextreal @ (ap@(ap@c_2Eextreal_2Eextreal__mul@(inj__ty_2Eextreal_2Eextreal @ fo__c_2Eextreal_2ENegInf))@(inj__ty_2Eextreal_2Eextreal @ fo__c_2Eextreal_2ENegInf))) = fo__c_2Eextreal_2EPosInf) & (((surj__ty_2Eextreal_2Eextreal @ (ap@(ap@c_2Eextreal_2Eextreal__mul@(inj__ty_2Eextreal_2Eextreal @ fo__c_2Eextreal_2ENegInf))@(inj__ty_2Eextreal_2Eextreal @ fo__c_2Eextreal_2EPosInf))) = fo__c_2Eextreal_2ENegInf) & (((surj__ty_2Eextreal_2Eextreal @ (ap@(ap@c_2Eextreal_2Eextreal__mul@(inj__ty_2Eextreal_2Eextreal @ fo__c_2Eextreal_2EPosInf))@(inj__ty_2Eextreal_2Eextreal @ fo__c_2Eextreal_2ENegInf))) = fo__c_2Eextreal_2ENegInf) & (((surj__ty_2Eextreal_2Eextreal @ (ap@(ap@c_2Eextreal_2Eextreal__mul@(inj__ty_2Eextreal_2Eextreal @ fo__c_2Eextreal_2EPosInf))@(inj__ty_2Eextreal_2Eextreal @ fo__c_2Eextreal_2EPosInf))) = fo__c_2Eextreal_2EPosInf) & (((surj__ty_2Eextreal_2Eextreal @ (ap@(ap@c_2Eextreal_2Eextreal__mul@(ap@c_2Eextreal_2ENormal@(inj__ty_2Erealax_2Ereal @ V0x)))@(inj__ty_2Eextreal_2Eextreal @ fo__c_2Eextreal_2ENegInf))) = (surj__ty_2Eextreal_2Eextreal @ (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Eextreal_2Eextreal)@(ap@(ap@(c_2Emin_2E_3D@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V0x))@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))@(ap@c_2Eextreal_2ENormal@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))@(ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Eextreal_2Eextreal)@(ap@(ap@c_2Erealax_2Ereal__lt@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(inj__ty_2Erealax_2Ereal @ V0x)))@(inj__ty_2Eextreal_2Eextreal @ fo__c_2Eextreal_2ENegInf))@(inj__ty_2Eextreal_2Eextreal @ fo__c_2Eextreal_2EPosInf))))) & (((surj__ty_2Eextreal_2Eextreal @ (ap@(ap@c_2Eextreal_2Eextreal__mul@(inj__ty_2Eextreal_2Eextreal @ fo__c_2Eextreal_2ENegInf))@(ap@c_2Eextreal_2ENormal@(inj__ty_2Erealax_2Ereal @ V1y)))) = (surj__ty_2Eextreal_2Eextreal @ (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Eextreal_2Eextreal)@(ap@(ap@(c_2Emin_2E_3D@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V1y))@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))@(ap@c_2Eextreal_2ENormal@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))@(ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Eextreal_2Eextreal)@(ap@(ap@c_2Erealax_2Ereal__lt@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(inj__ty_2Erealax_2Ereal @ V1y)))@(inj__ty_2Eextreal_2Eextreal @ fo__c_2Eextreal_2ENegInf))@(inj__ty_2Eextreal_2Eextreal @ fo__c_2Eextreal_2EPosInf))))) & (((surj__ty_2Eextreal_2Eextreal @ (ap@(ap@c_2Eextreal_2Eextreal__mul@(ap@c_2Eextreal_2ENormal@(inj__ty_2Erealax_2Ereal @ V0x)))@(inj__ty_2Eextreal_2Eextreal @ fo__c_2Eextreal_2EPosInf))) = (surj__ty_2Eextreal_2Eextreal @ (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Eextreal_2Eextreal)@(ap@(ap@(c_2Emin_2E_3D@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V0x))@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))@(ap@c_2Eextreal_2ENormal@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))@(ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Eextreal_2Eextreal)@(ap@(ap@c_2Erealax_2Ereal__lt@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(inj__ty_2Erealax_2Ereal @ V0x)))@(inj__ty_2Eextreal_2Eextreal @ fo__c_2Eextreal_2EPosInf))@(inj__ty_2Eextreal_2Eextreal @ fo__c_2Eextreal_2ENegInf))))) & (((surj__ty_2Eextreal_2Eextreal @ (ap@(ap@c_2Eextreal_2Eextreal__mul@(inj__ty_2Eextreal_2Eextreal @ fo__c_2Eextreal_2EPosInf))@(ap@c_2Eextreal_2ENormal@(inj__ty_2Erealax_2Ereal @ V1y)))) = (surj__ty_2Eextreal_2Eextreal @ (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Eextreal_2Eextreal)@(ap@(ap@(c_2Emin_2E_3D@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V1y))@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))@(ap@c_2Eextreal_2ENormal@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))@(ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Eextreal_2Eextreal)@(ap@(ap@c_2Erealax_2Ereal__lt@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(inj__ty_2Erealax_2Ereal @ V1y)))@(inj__ty_2Eextreal_2Eextreal @ fo__c_2Eextreal_2EPosInf))@(inj__ty_2Eextreal_2Eextreal @ fo__c_2Eextreal_2ENegInf))))) & ((surj__ty_2Eextreal_2Eextreal @ (ap@(ap@c_2Eextreal_2Eextreal__mul@(ap@c_2Eextreal_2ENormal@(inj__ty_2Erealax_2Ereal @ V0x)))@(ap@c_2Eextreal_2ENormal@(inj__ty_2Erealax_2Ereal @ V1y)))) = (surj__ty_2Eextreal_2Eextreal @ (ap@c_2Eextreal_2ENormal@(ap@(ap@c_2Erealax_2Ereal__mul@(inj__ty_2Erealax_2Ereal @ V0x))@(inj__ty_2Erealax_2Ereal @ V1y)))))))))))))))).
thf(conj_thm_2Eextreal_2Eextreal__not__infty,lemma,( ! [V0x:tp__ty_2Erealax_2Ereal] : ((~ ((surj__ty_2Eextreal_2Eextreal @ (ap@c_2Eextreal_2ENormal@(inj__ty_2Erealax_2Ereal @ V0x))) = fo__c_2Eextreal_2ENegInf)) & (~ ((surj__ty_2Eextreal_2Eextreal @ (ap@c_2Eextreal_2ENormal@(inj__ty_2Erealax_2Ereal @ V0x))) = fo__c_2Eextreal_2EPosInf))))).
thf(conj_thm_2Eextreal_2EEXTREAL__SUM__IMAGE__NORMAL,lemma,( ! [A_27a:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@ty_2Erealax_2Ereal)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V1s)) => ((surj__ty_2Eextreal_2Eextreal @ (ap@(ap@(c_2Eextreal_2EEXTREAL__SUM__IMAGE@A_27a)@(lam@A_27a@(^ [V2x:$i] : (ap@c_2Eextreal_2ENormal@(ap@V0f@V2x)))))@V1s)) = (surj__ty_2Eextreal_2Eextreal @ (ap@c_2Eextreal_2ENormal@(ap@(ap@(c_2Ereal__sigma_2EREAL__SUM__IMAGE@A_27a)@V0f)@V1s))))))))))).
thf(ax_thm_2Elebesgue_2Eprod__measure__def,axiom,( ! [A_27a:del]: ( ! [A_27b: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_27b@bool)@(ty_2Epair_2Eprod@(arr@(arr@A_27b@bool)@bool)@(arr@(arr@A_27b@bool)@ty_2Erealax_2Ereal)))) => ((ap@(ap@(c_2Elebesgue_2Eprod__measure@A_27a@A_27b)@V0m0)@V1m1) = (lam@(arr@(ty_2Epair_2Eprod@A_27a@A_27b)@bool)@(^ [V2a:$i] : (ap@c_2Eextreal_2Ereal@(ap@(ap@(c_2Elebesgue_2Eintegral@A_27a)@V0m0)@(lam@A_27a@(^ [V3s0:$i] : (ap@c_2Eextreal_2ENormal@(ap@(ap@(c_2Emeasure_2Emeasure@A_27b)@V1m1)@(ap@(ap@(c_2Epred__set_2EPREIMAGE@A_27b@(ty_2Epair_2Eprod@A_27a@A_27b))@(lam@A_27b@(^ [V4s1:$i] : (ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V3s0)@V4s1))))@V2a))))))))))))))))).
thf(ax_thm_2Elebesgue_2Eprod__measure__space__def,axiom,( ! [A_27a:del]: ( ! [A_27b: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_27b@bool)@(ty_2Epair_2Eprod@(arr@(arr@A_27b@bool)@bool)@(arr@(arr@A_27b@bool)@ty_2Erealax_2Ereal)))) => ((ap@(ap@(c_2Elebesgue_2Eprod__measure__space@A_27a@A_27b)@V0m0)@V1m1) = (ap@(ap@(c_2Epair_2E_2C@(arr@(ty_2Epair_2Eprod@A_27a@A_27b)@bool)@(ty_2Epair_2Eprod@(arr@(arr@(ty_2Epair_2Eprod@A_27a@A_27b)@bool)@bool)@(arr@(arr@(ty_2Epair_2Eprod@A_27a@A_27b)@bool)@ty_2Erealax_2Ereal)))@(ap@(ap@(c_2Epred__set_2ECROSS@A_27a@A_27b)@(ap@(c_2Emeasure_2Em__space@A_27a)@V0m0))@(ap@(c_2Emeasure_2Em__space@A_27b)@V1m1)))@(ap@(ap@(c_2Epair_2E_2C@(arr@(arr@(ty_2Epair_2Eprod@A_27a@A_27b)@bool)@bool)@(arr@(arr@(ty_2Epair_2Eprod@A_27a@A_27b)@bool)@ty_2Erealax_2Ereal))@(ap@(c_2Emeasure_2Esubsets@(ty_2Epair_2Eprod@A_27a@A_27b))@(ap@(ap@(c_2Emeasure_2Esigma@(ty_2Epair_2Eprod@A_27a@A_27b))@(ap@(ap@(c_2Epred__set_2ECROSS@A_27a@A_27b)@(ap@(c_2Emeasure_2Em__space@A_27a)@V0m0))@(ap@(c_2Emeasure_2Em__space@A_27b)@V1m1)))@(ap@(ap@(c_2Eutil__prob_2Eprod__sets@A_27a@A_27b)@(ap@(c_2Emeasure_2Emeasurable__sets@A_27a)@V0m0))@(ap@(c_2Emeasure_2Emeasurable__sets@A_27b)@V1m1)))))@(ap@(ap@(c_2Elebesgue_2Eprod__measure@A_27a@A_27b)@V0m0)@V1m1))))))))))).
thf(conj_thm_2Elebesgue_2Efinite__space__POW__integral__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)))) => ( ! [V1f:$i] : ((mem@V1f@(arr@A_27a@ty_2Eextreal_2Eextreal)) => (((p@(ap@(c_2Emeasure_2Emeasure__space@A_27a)@V0m)) & (((ap@(c_2Epred__set_2EPOW@A_27a)@(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))) & ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@(ap@(c_2Emeasure_2Em__space@A_27a)@V0m))) => ((~ ((surj__ty_2Eextreal_2Eextreal @ (ap@V1f@V2x)) = fo__c_2Eextreal_2ENegInf)) & (~ ((surj__ty_2Eextreal_2Eextreal @ (ap@V1f@V2x)) = fo__c_2Eextreal_2EPosInf))))))))) => ((surj__ty_2Eextreal_2Eextreal @ (ap@(ap@(c_2Elebesgue_2Eintegral@A_27a)@V0m)@V1f)) = (surj__ty_2Eextreal_2Eextreal @ (ap@(ap@(c_2Eextreal_2EEXTREAL__SUM__IMAGE@A_27a)@(lam@A_27a@(^ [V3x:$i] : (ap@(ap@c_2Eextreal_2Eextreal__mul@(ap@V1f@V3x))@(ap@c_2Eextreal_2ENormal@(ap@(ap@(c_2Emeasure_2Emeasure@A_27a)@V0m)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V3x)@(c_2Epred__set_2EEMPTY@A_27a))))))))@(ap@(c_2Emeasure_2Em__space@A_27a)@V0m))))))))))).
thf(conj_thm_2Elebesgue_2Efinite__POW__prod__measure__reduce,lemma,( ! [A_27a:del]: ( ! [A_27b: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_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)@V0m0)) & ((p@(ap@(c_2Emeasure_2Emeasure__space@A_27b)@V1m1)) & ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@(ap@(c_2Emeasure_2Em__space@A_27a)@V0m0))) & ((p@(ap@(c_2Epred__set_2EFINITE@A_27b)@(ap@(c_2Emeasure_2Em__space@A_27b)@V1m1))) & (((ap@(c_2Epred__set_2EPOW@A_27a)@(ap@(c_2Emeasure_2Em__space@A_27a)@V0m0)) = (ap@(c_2Emeasure_2Emeasurable__sets@A_27a)@V0m0)) & ((ap@(c_2Epred__set_2EPOW@A_27b)@(ap@(c_2Emeasure_2Em__space@A_27b)@V1m1)) = (ap@(c_2Emeasure_2Emeasurable__sets@A_27b)@V1m1))))))) => ( ! [V2a0:$i] : ((mem@V2a0@(arr@A_27a@bool)) => ( ! [V3a1:$i] : ((mem@V3a1@(arr@A_27b@bool)) => (((p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@bool))@V2a0)@(ap@(c_2Emeasure_2Emeasurable__sets@A_27a)@V0m0))) & (p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27b@bool))@V3a1)@(ap@(c_2Emeasure_2Emeasurable__sets@A_27b)@V1m1)))) => ((surj__ty_2Erealax_2Ereal @ (ap@(ap@(ap@(c_2Elebesgue_2Eprod__measure@A_27a@A_27b)@V0m0)@V1m1)@(ap@(ap@(c_2Epred__set_2ECROSS@A_27a@A_27b)@V2a0)@V3a1))) = (surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Erealax_2Ereal__mul@(ap@(ap@(c_2Emeasure_2Emeasure@A_27a)@V0m0)@V2a0))@(ap@(ap@(c_2Emeasure_2Emeasure@A_27b)@V1m1)@V3a1))))))))))))))))).
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_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_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_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(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_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__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_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_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_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_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_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_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_2Epair_2EPAIR__EQ,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1y:$i] : ((mem@V1y@A_27b) => ( ! [V2a:$i] : ((mem@V2a@A_27a) => ( ! [V3b:$i] : ((mem@V3b@A_27b) => (((ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V0x)@V1y) = (ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V2a)@V3b)) <=> ((V0x = V2a) & (V1y = V3b)))))))))))))).
thf(conj_thm_2Epair_2ECLOSED__PAIR__EQ,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1y:$i] : ((mem@V1y@A_27b) => ( ! [V2a:$i] : ((mem@V2a@A_27a) => ( ! [V3b:$i] : ((mem@V3b@A_27b) => (((ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V0x)@V1y) = (ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V2a)@V3b)) <=> ((V0x = V2a) & (V1y = V3b)))))))))))))).
thf(conj_thm_2Epair_2EABS__PAIR__THM,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0x:$i] : ((mem@V0x@(ty_2Epair_2Eprod@A_27a@A_27b)) => (? [V1q:$i] : ((mem@V1q@A_27a) & (? [V2r:$i] : ((mem@V2r@A_27b) & (V0x = (ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V1q)@V2r))))))))))).
thf(conj_thm_2Epair_2Epair__CASES,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0x:$i] : ((mem@V0x@(ty_2Epair_2Eprod@A_27a@A_27b)) => (? [V1q:$i] : ((mem@V1q@A_27a) & (? [V2r:$i] : ((mem@V2r@A_27b) & (V0x = (ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V1q)@V2r))))))))))).
thf(conj_thm_2Epair_2EFST,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1y:$i] : ((mem@V1y@A_27b) => ((ap@(c_2Epair_2EFST@A_27a@A_27b)@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V0x)@V1y)) = V0x)))))))).
thf(conj_thm_2Epair_2ESND,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1y:$i] : ((mem@V1y@A_27b) => ((ap@(c_2Epair_2ESND@A_27a@A_27b)@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V0x)@V1y)) = V1y)))))))).
thf(conj_thm_2Epair_2EUNCURRY__DEF,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@(arr@A_27b@A_27c))) => ( ! [V1x:$i] : ((mem@V1x@A_27a) => ( ! [V2y:$i] : ((mem@V2y@A_27b) => ((ap@(ap@(c_2Epair_2EUNCURRY@A_27a@A_27b@A_27c)@V0f)@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V1x)@V2y)) = (ap@(ap@V0f@V1x)@V2y)))))))))))).
thf(conj_thm_2Epred__set_2EEXTENSION,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ((V0s = V1t) <=> ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V0s)) <=> (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V1t)))))))))))).
thf(ax_thm_2Epred__set_2EGSPECIFICATION,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27b@(ty_2Epair_2Eprod@A_27a@bool))) => ( ! [V1v:$i] : ((mem@V1v@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V1v)@(ap@(c_2Epred__set_2EGSPEC@A_27a@A_27b)@V0f))) <=> (? [V2x:$i] : ((mem@V2x@A_27b) & ((ap@(ap@(c_2Epair_2E_2C@A_27a@bool)@V1v)@c_2Ebool_2ET) = (ap@V0f@V2x)))))))))))).
thf(conj_thm_2Epred__set_2ENOT__IN__EMPTY,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => (~ (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V0x)@(c_2Epred__set_2EEMPTY@A_27a)))))))).
thf(ax_thm_2Epred__set_2ESUBSET__DEF,axiom,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V0s)@V1t)) <=> ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V0s)) => (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V1t)))))))))))).
thf(conj_thm_2Epred__set_2EIN__UNION,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@(ap@(ap@(c_2Epred__set_2EUNION@A_27a)@V0s)@V1t))) <=> ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V0s)) | (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V1t)))))))))))).
thf(conj_thm_2Epred__set_2EIN__INTER,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@(ap@(ap@(c_2Epred__set_2EINTER@A_27a)@V0s)@V1t))) <=> ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V0s)) & (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V1t)))))))))))).
thf(ax_thm_2Epred__set_2EDISJOINT__DEF,axiom,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Epred__set_2EDISJOINT@A_27a)@V0s)@V1t)) <=> ((ap@(ap@(c_2Epred__set_2EINTER@A_27a)@V0s)@V1t) = (c_2Epred__set_2EEMPTY@A_27a))))))))).
thf(conj_thm_2Epred__set_2EIN__DISJOINT,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Epred__set_2EDISJOINT@A_27a)@V0s)@V1t)) <=> (~ (? [V2x:$i] : ((mem@V2x@A_27a) & ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V0s)) & (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V1t))))))))))))).
thf(conj_thm_2Epred__set_2EIN__SING,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1y:$i] : ((mem@V1y@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V0x)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V1y)@(c_2Epred__set_2EEMPTY@A_27a)))) <=> (V0x = V1y)))))))).
thf(conj_thm_2Epred__set_2EIN__BIGINTER,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1B:$i] : ((mem@V1B@(arr@(arr@A_27a@bool)@bool)) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V0x)@(ap@(c_2Epred__set_2EBIGINTER@A_27a)@V1B))) <=> ( ! [V2P:$i] : ((mem@V2P@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@bool))@V2P)@V1B)) => (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V0x)@V2P)))))))))))).
thf(conj_thm_2Epred__set_2EIN__CROSS,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1Q:$i] : ((mem@V1Q@(arr@A_27b@bool)) => ( ! [V2x:$i] : ((mem@V2x@(ty_2Epair_2Eprod@A_27a@A_27b)) => ((p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27b))@V2x)@(ap@(ap@(c_2Epred__set_2ECROSS@A_27a@A_27b)@V0P)@V1Q))) <=> ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@(ap@(c_2Epair_2EFST@A_27a@A_27b)@V2x))@V0P)) & (p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@(ap@(c_2Epair_2ESND@A_27a@A_27b)@V2x))@V1Q))))))))))))).
thf(conj_thm_2Epred__set_2ECROSS__EMPTY,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => (((ap@(ap@(c_2Epred__set_2ECROSS@A_27a@A_27b)@V0P)@(c_2Epred__set_2EEMPTY@A_27b)) = (c_2Epred__set_2EEMPTY@(ty_2Epair_2Eprod@A_27a@A_27b))) & ((ap@(ap@(c_2Epred__set_2ECROSS@A_27c@A_27a)@(c_2Epred__set_2EEMPTY@A_27c))@V0P) = (c_2Epred__set_2EEMPTY@(ty_2Epair_2Eprod@A_27c@A_27a)))))))))).
thf(conj_thm_2Epred__set_2EFINITE__CROSS,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1Q:$i] : ((mem@V1Q@(arr@A_27b@bool)) => (((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0P)) & (p@(ap@(c_2Epred__set_2EFINITE@A_27b)@V1Q))) => (p@(ap@(c_2Epred__set_2EFINITE@(ty_2Epair_2Eprod@A_27a@A_27b))@(ap@(ap@(c_2Epred__set_2ECROSS@A_27a@A_27b)@V0P)@V1Q))))))))))).
thf(conj_thm_2Epred__set_2EIN__POW,lemma,( ! [A_27a:del]: ( ! [V0set:$i] : ((mem@V0set@(arr@A_27a@bool)) => ( ! [V1e:$i] : ((mem@V1e@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@bool))@V1e)@(ap@(c_2Epred__set_2EPOW@A_27a)@V0set))) <=> (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V1e)@V0set))))))))).
thf(conj_thm_2Epred__set_2EIN__PREIMAGE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27b@bool)) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@(ap@(ap@(c_2Epred__set_2EPREIMAGE@A_27a@A_27b)@V0f)@V1s))) <=> (p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@(ap@V0f@V2x))@V1s)))))))))))).
thf(conj_thm_2Ereal_2EREAL__MUL__LZERO,lemma,( ! [V0x:tp__ty_2Erealax_2Ereal] : ((surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Erealax_2Ereal__mul@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(inj__ty_2Erealax_2Ereal @ V0x))) = (surj__ty_2Erealax_2Ereal @ (ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))).
thf(conj_thm_2Ereal_2EREAL__LE__MUL,lemma,( ! [V0x:tp__ty_2Erealax_2Ereal] : ( ! [V1y:tp__ty_2Erealax_2Ereal] : (((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 @ V0x))) & (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 @ V1y)))) => (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(ap@(ap@c_2Erealax_2Ereal__mul@(inj__ty_2Erealax_2Ereal @ V0x))@(inj__ty_2Erealax_2Ereal @ V1y)))))))).
thf(conj_thm_2Ereal_2EREAL__ADD__RDISTRIB,lemma,( ! [V0x:tp__ty_2Erealax_2Ereal] : ( ! [V1y:tp__ty_2Erealax_2Ereal] : ( ! [V2z:tp__ty_2Erealax_2Ereal] : ((surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Erealax_2Ereal__mul@(ap@(ap@c_2Erealax_2Ereal__add@(inj__ty_2Erealax_2Ereal @ V0x))@(inj__ty_2Erealax_2Ereal @ V1y)))@(inj__ty_2Erealax_2Ereal @ V2z))) = (surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Erealax_2Ereal__add@(ap@(ap@c_2Erealax_2Ereal__mul@(inj__ty_2Erealax_2Ereal @ V0x))@(inj__ty_2Erealax_2Ereal @ V2z)))@(ap@(ap@c_2Erealax_2Ereal__mul@(inj__ty_2Erealax_2Ereal @ V1y))@(inj__ty_2Erealax_2Ereal @ V2z))))))))).
thf(conj_thm_2Ereal__sigma_2EREAL__SUM__IMAGE__POS,lemma,( ! [A_27a:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@ty_2Erealax_2Ereal)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => (((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V1s)) & ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V1s)) => (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(ap@V0f@V2x))))))) => (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(ap@(ap@(c_2Ereal__sigma_2EREAL__SUM__IMAGE@A_27a)@V0f)@V1s)))))))))).
thf(conj_thm_2Ereal__sigma_2EREAL__SUM__IMAGE__ADD,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s)) => ( ! [V1f:$i] : ((mem@V1f@(arr@A_27a@ty_2Erealax_2Ereal)) => ( ! [V2f_27:$i] : ((mem@V2f_27@(arr@A_27a@ty_2Erealax_2Ereal)) => ((surj__ty_2Erealax_2Ereal @ (ap@(ap@(c_2Ereal__sigma_2EREAL__SUM__IMAGE@A_27a)@(lam@A_27a@(^ [V3x:$i] : (ap@(ap@c_2Erealax_2Ereal__add@(ap@V1f@V3x))@(ap@V2f_27@V3x)))))@V0s)) = (surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Erealax_2Ereal__add@(ap@(ap@(c_2Ereal__sigma_2EREAL__SUM__IMAGE@A_27a)@V1f)@V0s))@(ap@(ap@(c_2Ereal__sigma_2EREAL__SUM__IMAGE@A_27a)@V2f_27)@V0s))))))))))))).
thf(conj_thm_2Ereal__sigma_2EREAL__SUM__IMAGE__EQ,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1f:$i] : ((mem@V1f@(arr@A_27a@ty_2Erealax_2Ereal)) => ( ! [V2f_27:$i] : ((mem@V2f_27@(arr@A_27a@ty_2Erealax_2Ereal)) => (((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s)) & ( ! [V3x:$i] : ((mem@V3x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3x)@V0s)) => ((surj__ty_2Erealax_2Ereal @ (ap@V1f@V3x)) = (surj__ty_2Erealax_2Ereal @ (ap@V2f_27@V3x))))))) => ((surj__ty_2Erealax_2Ereal @ (ap@(ap@(c_2Ereal__sigma_2EREAL__SUM__IMAGE@A_27a)@V1f)@V0s)) = (surj__ty_2Erealax_2Ereal @ (ap@(ap@(c_2Ereal__sigma_2EREAL__SUM__IMAGE@A_27a)@V2f_27)@V0s)))))))))))).
thf(conj_thm_2Esat_2ENOT__NOT,lemma,( ! [V0t:$i] : ((mem@V0t@bool) => ((~ (~ (p@V0t))) <=> (p@V0t))))).
thf(conj_thm_2Esat_2EAND__INV__IMP,lemma,( ! [V0A:$i] : ((mem@V0A@bool) => ((p@V0A) => ((~ (p@V0A)) => $false))))).
thf(conj_thm_2Esat_2EOR__DUAL2,lemma,( ! [V0A:$i] : ((mem@V0A@bool) => ( ! [V1B:$i] : ((mem@V1B@bool) => (((~ ((p@V0A) | (p@V1B))) => $false) <=> (((p@V0A) => $false) => ((~ (p@V1B)) => $false)))))))).
thf(conj_thm_2Esat_2EOR__DUAL3,lemma,( ! [V0A:$i] : ((mem@V0A@bool) => ( ! [V1B:$i] : ((mem@V1B@bool) => (((~ ((~ (p@V0A)) | (p@V1B))) => $false) <=> ((p@V0A) => ((~ (p@V1B)) => $false)))))))).
thf(conj_thm_2Esat_2EAND__INV2,lemma,( ! [V0A:$i] : ((mem@V0A@bool) => (((~ (p@V0A)) => $false) => (((p@V0A) => $false) => $false))))).
thf(conj_thm_2Esat_2Edc__eq,lemma,( ! [V0p:$i] : ((mem@V0p@bool) => ( ! [V1q:$i] : ((mem@V1q@bool) => ( ! [V2r:$i] : ((mem@V2r@bool) => (((p@V0p) <=> ((p@V1q) <=> (p@V2r))) <=> (((p@V0p) | ((p@V1q) | (p@V2r))) & (((p@V0p) | ((~ (p@V2r)) | (~ (p@V1q)))) & (((p@V1q) | ((~ (p@V2r)) | (~ (p@V0p)))) & ((p@V2r) | ((~ (p@V1q)) | (~ (p@V0p))))))))))))))).
thf(conj_thm_2Esat_2Edc__conj,lemma,( ! [V0p:$i] : ((mem@V0p@bool) => ( ! [V1q:$i] : ((mem@V1q@bool) => ( ! [V2r:$i] : ((mem@V2r@bool) => (((p@V0p) <=> ((p@V1q) & (p@V2r))) <=> (((p@V0p) | ((~ (p@V1q)) | (~ (p@V2r)))) & (((p@V1q) | (~ (p@V0p))) & ((p@V2r) | (~ (p@V0p))))))))))))).
thf(conj_thm_2Esat_2Edc__disj,lemma,( ! [V0p:$i] : ((mem@V0p@bool) => ( ! [V1q:$i] : ((mem@V1q@bool) => ( ! [V2r:$i] : ((mem@V2r@bool) => (((p@V0p) <=> ((p@V1q) | (p@V2r))) <=> (((p@V0p) | (~ (p@V1q))) & (((p@V0p) | (~ (p@V2r))) & ((p@V1q) | ((p@V2r) | (~ (p@V0p)))))))))))))).
thf(conj_thm_2Esat_2Edc__imp,lemma,( ! [V0p:$i] : ((mem@V0p@bool) => ( ! [V1q:$i] : ((mem@V1q@bool) => ( ! [V2r:$i] : ((mem@V2r@bool) => (((p@V0p) <=> ((p@V1q) => (p@V2r))) <=> (((p@V0p) | (p@V1q)) & (((p@V0p) | (~ (p@V2r))) & ((~ (p@V1q)) | ((p@V2r) | (~ (p@V0p)))))))))))))).
thf(conj_thm_2Esat_2Edc__neg,lemma,( ! [V0p:$i] : ((mem@V0p@bool) => ( ! [V1q:$i] : ((mem@V1q@bool) => (((p@V0p) <=> (~ (p@V1q))) <=> (((p@V0p) | (p@V1q)) & ((~ (p@V1q)) | (~ (p@V0p)))))))))).
thf(conj_thm_2Esat_2Epth__ni1,lemma,( ! [V0p:$i] : ((mem@V0p@bool) => ( ! [V1q:$i] : ((mem@V1q@bool) => ((~ ((p@V0p) => (p@V1q))) => (p@V0p))))))).
thf(conj_thm_2Esat_2Epth__ni2,lemma,( ! [V0p:$i] : ((mem@V0p@bool) => ( ! [V1q:$i] : ((mem@V1q@bool) => ((~ ((p@V0p) => (p@V1q))) => (~ (p@V1q)))))))).
thf(conj_thm_2Esat_2Epth__no1,lemma,( ! [V0p:$i] : ((mem@V0p@bool) => ( ! [V1q:$i] : ((mem@V1q@bool) => ((~ ((p@V0p) | (p@V1q))) => (~ (p@V0p)))))))).
thf(conj_thm_2Esat_2Epth__no2,lemma,( ! [V0p:$i] : ((mem@V0p@bool) => ( ! [V1q:$i] : ((mem@V1q@bool) => ((~ ((p@V0p) | (p@V1q))) => (~ (p@V1q)))))))).
thf(conj_thm_2Esat_2Epth__nn,lemma,( ! [V0p:$i] : ((mem@V0p@bool) => ((~ (~ (p@V0p))) => (p@V0p))))).
thf(ax_thm_2Eutil__prob_2Eprod__sets__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0a:$i] : ((mem@V0a@(arr@(arr@A_27a@bool)@bool)) => ( ! [V1b:$i] : ((mem@V1b@(arr@(arr@A_27b@bool)@bool)) => ((ap@(ap@(c_2Eutil__prob_2Eprod__sets@A_27a@A_27b)@V0a)@V1b) = (ap@(c_2Epred__set_2EGSPEC@(arr@(ty_2Epair_2Eprod@A_27a@A_27b)@bool)@(ty_2Epair_2Eprod@(arr@A_27a@bool)@(arr@A_27b@bool)))@(ap@(c_2Epair_2EUNCURRY@(arr@A_27a@bool)@(arr@A_27b@bool)@(ty_2Epair_2Eprod@(arr@(ty_2Epair_2Eprod@A_27a@A_27b)@bool)@bool))@(lam@(arr@A_27a@bool)@(^ [V2s:$i] : (lam@(arr@A_27b@bool)@(^ [V3t:$i] : (ap@(ap@(c_2Epair_2E_2C@(arr@(ty_2Epair_2Eprod@A_27a@A_27b)@bool)@bool)@(ap@(ap@(c_2Epred__set_2ECROSS@A_27a@A_27b)@V2s)@V3t))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@bool))@V2s)@V0a))@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27b@bool))@V3t)@V1b))))))))))))))))).
thf(conj_thm_2Elebesgue_2Emeasure__space__finite__prod__measure__POW1,conjecture,( ! [A_27a:del]: ( ! [A_27b: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_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)@V0m0)) & ((p@(ap@(c_2Emeasure_2Emeasure__space@A_27b)@V1m1)) & ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@(ap@(c_2Emeasure_2Em__space@A_27a)@V0m0))) & ((p@(ap@(c_2Epred__set_2EFINITE@A_27b)@(ap@(c_2Emeasure_2Em__space@A_27b)@V1m1))) & (((ap@(c_2Epred__set_2EPOW@A_27a)@(ap@(c_2Emeasure_2Em__space@A_27a)@V0m0)) = (ap@(c_2Emeasure_2Emeasurable__sets@A_27a)@V0m0)) & ((ap@(c_2Epred__set_2EPOW@A_27b)@(ap@(c_2Emeasure_2Em__space@A_27b)@V1m1)) = (ap@(c_2Emeasure_2Emeasurable__sets@A_27b)@V1m1))))))) => (p@(ap@(c_2Emeasure_2Emeasure__space@(ty_2Epair_2Eprod@A_27a@A_27b))@(ap@(ap@(c_2Elebesgue_2Eprod__measure__space@A_27a@A_27b)@V0m0)@V1m1))))))))))).
