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 Th72;
then A1: monotoneclass Z is SigmaField of Omega by Th70;
Z c= monotoneclass Z by Def9;
hence sigma Z c= monotoneclass Z by A1, PROB_1:def 9; :: according to XBOOLE_0:def 10 :: thesis: monotoneclass Z c= sigma Z
( sigma Z is MonotoneClass of Omega & Z c= sigma Z ) by Th70, PROB_1:def 9;
hence monotoneclass Z c= sigma Z by Def9; :: thesis: verum