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

now :: thesis: for t being object st t in ([#] Sigma) /\ (great_eq_dom (X,r)) holds
t in { t where t is Element of Omega : r <= X . t }

let t be object ; :: thesis: ( t in ([#] Sigma) /\ (great_eq_dom (X,r)) implies t in { t where t is Element of Omega : r <= X . t } )
assume t in ([#] Sigma) /\ (great_eq_dom (X,r)) ; :: thesis: t in { t where t is Element of Omega : r <= X . t }
then t in great_eq_dom (X,r) by XBOOLE_0:def 4;
then ( t in dom X & r <= X . t ) by MESFUNC1:def 14;
hence t in { t where t is Element of Omega : r <= X . t } ; :: thesis: verum

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;

now :: thesis: for x being object st x in { t where t is Element of Omega : r <= X . t } holds
x in ([#] Sigma) /\ (great_eq_dom (X,r))

let x be object ; :: thesis: ( x in { t where t is Element of Omega : r <= X . t } implies x in ([#] Sigma) /\ (great_eq_dom (X,r)) )
assume x in { t where t is Element of Omega : r <= X . t } ; :: thesis: x in ([#] Sigma) /\ (great_eq_dom (X,r))
then A8: ex t being Element of Omega st
( x = t & r <= X . t ) ;
then x in great_eq_dom (X,r) by A7, MESFUNC1:def 14;
hence x in ([#] Sigma) /\ (great_eq_dom (X,r)) by A8, XBOOLE_0:def 4; :: thesis: verum

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

proof

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

end;

A11: jj in REAL by XREAL_0:def 1;
(P2M P) . K <= jj by PROB_1:35;
then A12: (P2M P) . K < +infty by XXREAL_0:2, XXREAL_0:9, A11;
X is_integrable_on P2M P by A3;
then r * ((P2M P) . K) <= Integral ((P2M P),(X | K)) by A7, A12, A10, Th2;
then r * PMK <= Integral ((P2M P),(X | K)) by EXTREAL1:1;
then r * PMK <= Integral ((P2M P),X) by A9, XXREAL_0:2;
then (r * PMK) / r <= IX / r by A1, XREAL_1:72;
then PMK <= IX / r by A1, XCMPLX_1:89;
hence P . { t where t is Element of Omega : r <= X . t } <= (expect (X,P)) / r by A3, Def4; :: thesis: verum