let R1, R2 be SigmaField of Omega; :: thesis: ( X c= R1 & ( for Z being set st X c= Z & Z is SigmaField of Omega holds

R1 c= Z ) & X c= R2 & ( for Z being set st X c= Z & Z is SigmaField of Omega holds

R2 c= Z ) implies R1 = R2 )

assume ( X c= R1 & ( for Z being set st X c= Z & Z is SigmaField of Omega holds

R1 c= Z ) & X c= R2 & ( for Z being set st X c= Z & Z is SigmaField of Omega holds

R2 c= Z ) ) ; :: thesis: R1 = R2

then ( R1 c= R2 & R2 c= R1 ) ;

hence R1 = R2 by XBOOLE_0:def 10; :: thesis: verum

R1 c= Z ) & X c= R2 & ( for Z being set st X c= Z & Z is SigmaField of Omega holds

R2 c= Z ) implies R1 = R2 )

assume ( X c= R1 & ( for Z being set st X c= Z & Z is SigmaField of Omega holds

R1 c= Z ) & X c= R2 & ( for Z being set st X c= Z & Z is SigmaField of Omega holds

R2 c= Z ) ) ; :: thesis: R1 = R2

then ( R1 c= R2 & R2 c= R1 ) ;

hence R1 = R2 by XBOOLE_0:def 10; :: thesis: verum