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

( 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