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 A c= B ; :: thesis: A is measure_zero of M
then M . A <= M . B by Th8;
then A1: M . A <= 0. by Def4;
0. <= M . A by Def2;
then M . A = 0. by A1;
hence A is measure_zero of M by Def4; :: thesis: verum