let T1, T2 be TopSpace; :: thesis: ( the carrier of T1 = the carrier of T2 & ( for A1 being Subset of T1

for A2 being Subset of T2 st A1 = A2 holds

Int A1 = Int A2 ) implies the topology of T1 = the topology of T2 )

assume that

A1: the carrier of T1 = the carrier of T2 and

A2: for A1 being Subset of T1

for A2 being Subset of T2 st A1 = A2 holds

Int A1 = Int A2 ; :: thesis: the topology of T1 = the topology of T2

for A2 being Subset of T2 st A1 = A2 holds

Int A1 = Int A2 ) implies the topology of T1 = the topology of T2 )

assume that

A1: the carrier of T1 = the carrier of T2 and

A2: for A1 being Subset of T1

for A2 being Subset of T2 st A1 = A2 holds

Int A1 = Int A2 ; :: thesis: the topology of T1 = the topology of T2

now :: thesis: for A1 being Subset of T1

for A2 being Subset of T2 st A1 = A2 holds

Cl A1 = Cl A2

hence
the topology of T1 = the topology of T2
by A1, Th8; :: thesis: verumfor A2 being Subset of T2 st A1 = A2 holds

Cl A1 = Cl A2

let A1 be Subset of T1; :: thesis: for A2 being Subset of T2 st A1 = A2 holds

Cl A1 = Cl A2

let A2 be Subset of T2; :: thesis: ( A1 = A2 implies Cl A1 = Cl A2 )

assume A1 = A2 ; :: thesis: Cl A1 = Cl A2

then Int (A1 `) = Int (A2 `) by A1, A2;

hence Cl A1 = (Int (A2 `)) ` by A1, TDLAT_3:1

.= Cl A2 by TDLAT_3:1 ;

:: thesis: verum

end;Cl A1 = Cl A2

let A2 be Subset of T2; :: thesis: ( A1 = A2 implies Cl A1 = Cl A2 )

assume A1 = A2 ; :: thesis: Cl A1 = Cl A2

then Int (A1 `) = Int (A2 `) by A1, A2;

hence Cl A1 = (Int (A2 `)) ` by A1, TDLAT_3:1

.= Cl A2 by TDLAT_3:1 ;

:: thesis: verum