let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for M being sigma_Measure of Sigma
for A, B being set st A in Sigma & B in Sigma & A c= B & M . B < +infty holds
M . A in REAL
let Sigma be SigmaField of Omega; :: thesis: for M being sigma_Measure of Sigma
for A, B being set st A in Sigma & B in Sigma & A c= B & M . B < +infty holds
M . A in REAL
let M be sigma_Measure of Sigma; :: thesis: for A, B being set st A in Sigma & B in Sigma & A c= B & M . B < +infty holds
M . A in REAL
let A, B be set ; :: thesis: ( A in Sigma & B in Sigma & A c= B & M . B < +infty implies M . A in REAL )
assume ( A in Sigma & B in Sigma & A c= B & M . B < +infty ) ; :: thesis: M . A in REAL
then ( M . A <> -infty & M . A <> +infty ) by MEASURE1:31, MEASURE1:def 2;
hence M . A in REAL by XXREAL_0:14; :: thesis: verum