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

Cl A1 = Cl 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

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

hence the topology of T1 = the topology of T2 ; :: thesis: verum

for A2 being Subset of T2 st A1 = A2 holds

Cl A1 = Cl 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

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

now :: thesis: for A being set holds

( ( A is closed Subset of T1 implies A is closed Subset of T2 ) & ( A is closed Subset of T2 implies A is closed Subset of T1 ) )

then
TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #)
by Th6;( ( A is closed Subset of T1 implies A is closed Subset of T2 ) & ( A is closed Subset of T2 implies A is closed Subset of T1 ) )

let A be set ; :: thesis: ( ( A is closed Subset of T1 implies A is closed Subset of T2 ) & ( A is closed Subset of T2 implies A is closed Subset of T1 ) )

thus ( A is closed Subset of T1 implies A is closed Subset of T2 ) :: thesis: ( A is closed Subset of T2 implies A is closed Subset of T1 )

then reconsider A2 = A as closed Subset of T2 ;

reconsider A1 = A2 as Subset of T1 by A1;

Cl A2 = A2 by PRE_TOPC:22;

then Cl A1 = A1 by A2;

hence A is closed Subset of T1 ; :: thesis: verum

end;thus ( A is closed Subset of T1 implies A is closed Subset of T2 ) :: thesis: ( A is closed Subset of T2 implies A is closed Subset of T1 )

proof

assume
A is closed Subset of T2
; :: thesis: A is closed Subset of T1
assume
A is closed Subset of T1
; :: thesis: A is closed Subset of T2

then reconsider A1 = A as closed Subset of T1 ;

reconsider A2 = A1 as Subset of T2 by A1;

Cl A1 = A1 by PRE_TOPC:22;

then Cl A2 = A2 by A2;

hence A is closed Subset of T2 ; :: thesis: verum

end;then reconsider A1 = A as closed Subset of T1 ;

reconsider A2 = A1 as Subset of T2 by A1;

Cl A1 = A1 by PRE_TOPC:22;

then Cl A2 = A2 by A2;

hence A is closed Subset of T2 ; :: thesis: verum

then reconsider A2 = A as closed Subset of T2 ;

reconsider A1 = A2 as Subset of T1 by A1;

Cl A2 = A2 by PRE_TOPC:22;

then Cl A1 = A1 by A2;

hence A is closed Subset of T1 ; :: thesis: verum

hence the topology of T1 = the topology of T2 ; :: thesis: verum