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 that
A2: for G being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T holds R1 c= G and
A3: for G being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T holds R2 c= G ; :: thesis: R1 = R2
A4: R1 c= R2 by A2;
R2 c= R1 by A3;
hence R1 = R2 by A4, XBOOLE_0:def 10; :: thesis: verum