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