let R1, R2 be MonotoneClass of Omega; :: thesis: ( X c= R1 & ( for Z being set st X c= Z & Z is MonotoneClass of Omega holds
R1 c= Z ) & X c= R2 & ( for Z being set st X c= Z & Z is MonotoneClass of Omega holds
R2 c= Z ) implies R1 = R2 )
assume that
A1: X c= R1 and
A2: ( ( for Z being set st X c= Z & Z is MonotoneClass of Omega holds
R1 c= Z ) & X c= R2 ) and
A3: for Z being set st X c= Z & Z is MonotoneClass of Omega holds
R2 c= Z ; :: thesis: R1 = R2
thus R1 c= R2 by A2; :: according to XBOOLE_0:def 10 :: thesis: R2 c= R1
thus R2 c= R1 by A1, A3; :: thesis: verum