let X be non empty set ; :: thesis: for F being Field_Subset of X
for L being SetSequence of X st rng L is MonotoneClass of X & F c= rng L holds
( sigma F = monotoneclass F & sigma F c= rng L )
let F be Field_Subset of X; :: thesis: for L being SetSequence of X st rng L is MonotoneClass of X & F c= rng L holds
( sigma F = monotoneclass F & sigma F c= rng L )
let L be SetSequence of X; :: thesis: ( rng L is MonotoneClass of X & F c= rng L implies ( sigma F = monotoneclass F & sigma F c= rng L ) )
assume A1: ( rng L is MonotoneClass of X & F c= rng L ) ; :: thesis: ( sigma F = monotoneclass F & sigma F c= rng L )
thus sigma F = monotoneclass F by PROB_3:73; :: thesis: sigma F c= rng L
hence sigma F c= rng L by A1, PROB_3:def 11; :: thesis: verum