let Omega be non empty set ; :: thesis: for Z being Field_Subset of Omega holds sigma Z = monotoneclass Z
let Z be Field_Subset of Omega; :: thesis: sigma Z = monotoneclass Z
thus sigma Z c= monotoneclass Z :: according to XBOOLE_0:def 10 :: thesis: monotoneclass Z c= sigma Z

proof

monotoneclass Z is Field_Subset of Omega by Th78;
then A1: monotoneclass Z is SigmaField of Omega by Th75;
Z c= monotoneclass Z by Def15;
hence sigma Z c= monotoneclass Z by A1, PROB_1:def 14; :: thesis: verum

end;

A2: sigma Z is MonotoneClass of Omega by Th75;
Z c= sigma Z by PROB_1:def 14;
hence monotoneclass Z c= sigma Z by A2, Def15; :: thesis: verum