let X be set ; :: thesis: for S being SigmaField of X

for M being sigma_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 SigmaField of X; :: thesis: for M being sigma_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 sigma_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 Def7;

0. <= M . A by Def2;

then M . A = 0. by A1;

hence A is measure_zero of M by Def7; :: thesis: verum

for M being sigma_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 SigmaField of X; :: thesis: for M being sigma_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 sigma_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 Def7;

0. <= M . A by Def2;

then M . A = 0. by A1;

hence A is measure_zero of M by Def7; :: thesis: verum