let R1, R2 be compl-closed all-open-containing closed_for_countable_unions Subset-Family of T; :: thesis: ( ( for G being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T holds R1 c= G ) & ( for G being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T holds R2 c= G ) implies R1 = R2 )
assume ( ( for G being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T holds R1 c= G ) & ( for G being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T holds R2 c= G ) ) ; :: thesis: R1 = R2
then ( R1 c= R2 & R2 c= R1 ) ;
hence R1 = R2 by XBOOLE_0:def 10; :: thesis: verum