let T1, T2 be TopSpace; :: thesis: ( ( for A being set holds
( A is open Subset of T1 iff A is open Subset of T2 ) ) implies ( the carrier of T1 = the carrier of T2 & the topology of T1 c= the topology of T2 ) )
assume A1: for A being set holds
( A is open Subset of T1 iff A is open Subset of T2 ) ; :: thesis: ( the carrier of T1 = the carrier of T2 & the topology of T1 c= the topology of T2 )
the carrier of T2 = [#] T2 ;
then A2: the carrier of T2 is Subset of T1 by A1;
the carrier of T1 = [#] T1 ;
then A3: the carrier of T1 is Subset of T2 by A1;
hence the carrier of T1 = the carrier of T2 by A2; :: thesis: the topology of T1 c= the topology of T2
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in the topology of T1 or a in the topology of T2 )
assume A4: a in the topology of T1 ; :: thesis: a in the topology of T2
then reconsider a = a as Subset of T1 ;
reconsider b = a as Subset of T2 by A3, A2, XBOOLE_0:def 10;
a is open by A4;
then b is open by A1;
hence a in the topology of T2 ; :: thesis: verum