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 & ( for Z being set st X c= Z & Z is MonotoneClass of Omega holds
R1 c= Z ) ) and
A2: ( X c= R2 & ( 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 A1, A2; :: according to XBOOLE_0:def 10 :: thesis: R2 c= R1
thus R2 c= R1 by A1, A2; :: thesis: verum