let X be non empty set ; :: thesis: for F being Field_Subset of X
for K being Subset-Family of X st K is MonotoneClass of X & F c= K holds
( sigma F = monotoneclass F & sigma F c= K )
let F be Field_Subset of X; :: thesis: for K being Subset-Family of X st K is MonotoneClass of X & F c= K holds
( sigma F = monotoneclass F & sigma F c= K )
let K be Subset-Family of X; :: thesis: ( K is MonotoneClass of X & F c= K implies ( sigma F = monotoneclass F & sigma F c= K ) )
assume that
A1: K is MonotoneClass of X and
A2: F c= K ; :: thesis: ( sigma F = monotoneclass F & sigma F c= K )
thus sigma F = monotoneclass F by PROB_3:73; :: thesis: sigma F c= K
hence sigma F c= K by A1, A2, PROB_3:def 11; :: thesis: verum