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 } ;
consider S being Element of Sigma such that
A4: S = Omega and
A5: X is_measurable_on S by Def2;

now

let t be set ; :: thesis: ( t in S /\ (great_eq_dom X,r) implies t in { t where t is Element of Omega : r <= X . t } )
assume t in S /\ (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 15;
hence t in { t where t is Element of Omega : r <= X . t } ; :: thesis: verum

end;

then A6: S /\ (great_eq_dom X,r) c= { t where t is Element of Omega : r <= X . t } by TARSKI:def 3;
A7: dom X = S by A4, FUNCT_2:def 1;

now

let x be set ; :: thesis: ( x in { t where t is Element of Omega : r <= X . t } implies x in S /\ (great_eq_dom X,r) )
assume x in { t where t is Element of Omega : r <= X . t } ; :: thesis: x in S /\ (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 A4, A7, MESFUNC1:def 15;
hence x in S /\ (great_eq_dom X,r) by A4, A8, XBOOLE_0:def 4; :: thesis: verum

end;

then { t where t is Element of Omega : r <= X . t } c= S /\ (great_eq_dom X,r) by TARSKI:def 3;
then S /\ (great_eq_dom X,r) = { t where t is Element of Omega : r <= X . t } by A6, XBOOLE_0:def 10;
then reconsider K = { t where t is Element of Omega : r <= X . t } as Element of Sigma by A5, A7, MESFUNC6:13;
Integral (P2M P),(X | K) <= Integral (P2M P),(X | S) by A2, A4, A5, A7, MESFUNC6:87;
then A9: Integral (P2M P),(X | K) <= Integral (P2M P),X by A4, FUNCT_2:40;
expect X,P = Integral (P2M P),X by A3, Def4;
then reconsider IX = Integral (P2M P),X as Element of REAL ;
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;

(P2M P) . K <= 1 by PROB_1:71;
then A11: (P2M P) . K < +infty by XXREAL_0:2, XXREAL_0:9;
X is_integrable_on P2M P by A3, Def3;
then (R_EAL r) * ((P2M P) . K) <= Integral (P2M P),(X | K) by A4, A7, A11, A10, Th2;
then r * PMK <= Integral (P2M P),(X | K) by EXTREAL1:13;
then r * PMK <= Integral (P2M P),X by A9, XXREAL_0:2;
then (r * PMK) / r <= IX / r by A1, XREAL_1:74;
then PMK <= IX / r by A1, XCMPLX_1:90;
hence P . { t where t is Element of Omega : r <= X . t } <= (expect X,P) / r by A3, Def4; :: thesis: verum