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

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