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

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