let X be set ; :: thesis: for S being Field_Subset of X
for M being Measure of S
for A being Element of S
for B being measure_zero of M st A c= B holds
A is measure_zero of M
let S be Field_Subset of X; :: thesis: for M being Measure of S
for A being Element of S
for B being measure_zero of M st A c= B holds
A is measure_zero of M
let M be Measure of S; :: thesis: for A being Element of S
for B being measure_zero of M st A c= B holds
A is measure_zero of M
let A be Element of S; :: thesis: for B being measure_zero of M st A c= B holds
A is measure_zero of M
let B be measure_zero of M; :: thesis: ( A c= B implies A is measure_zero of M )
assume A1: A c= B ; :: thesis: A is measure_zero of M
( 0. <= M . A & M . A <= M . B ) by A1, Def4, Th25;
then ( 0. <= M . A & M . A <= 0. ) by Def7;
then M . A = 0. by XXREAL_0:1;
hence A is measure_zero of M by Def7; :: thesis: verum