let Omega be non empty set ; :: thesis:
let r be Real; :: thesis:
let Sigma be SigmaField of Omega; :: thesis:
let P be Probability of Sigma; :: thesis:
let X be Real-Valued-Random-Variable of Sigma; :: thesis:
assume that
A1: 0 < r and
A2: X is nonnegative and
A3: X is_integrable_on P ; :: thesis:
set PM = P2M P;
set K = { t where t is Element of Omega : r <= X . t } ;
set S = [#] Sigma;

end;

then A6: ([#] Sigma) /\ (great_eq_dom (X,r)) c= { t where t is Element of Omega : r <= X . t } ;
A7: dom X = [#] Sigma by FUNCT_2:def 1;

end;

then { t where t is Element of Omega : r <= X . t } c= ([#] Sigma) /\ (great_eq_dom (X,r)) ;
then ([#] Sigma) /\ (great_eq_dom (X,r)) = { t where t is Element of Omega : r <= X . t } by A6;
then reconsider K = { t where t is Element of Omega : r <= X . t } as Element of Sigma by A7, MESFUNC6:13;
Integral ((P2M P),(X | K)) <= Integral ((P2M P),(X | ([#] Sigma))) by A2, A7, MESFUNC6:87;
then A9: Integral ((P2M P),(X | K)) <= Integral ((P2M P),X) ;
expect (X,P) = Integral ((P2M P),X) by A3, Def4;
then reconsider IX = Integral ((P2M P),X) as Element of REAL by XREAL_0:def 1;
reconsider PMK = (P2M P) . K as Element of REAL by XXREAL_0:14;
A10: for t being Element of Omega st t in K holds
r <= X . t

let t be Element of Omega; :: thesis:
assume t in K ; :: thesis:
then ex s being Element of Omega st
( s = t & r <= X . s ) ;
hence r <= X . t ; :: thesis:

end;