for X being non empty set
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 )