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
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; :: according to XBOOLE_0:def 10 :: thesis: monotoneclass Z c= sigma Z
( sigma Z is MonotoneClass of Omega & Z c= sigma Z ) by Th75, PROB_1:def 14;
hence monotoneclass Z c= sigma Z by Def15; :: thesis: verum