let X1, X2 be TopSpace; for D1 being Subset of X1
for D2 being Subset of X2 st D1 = D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) holds
Cl D1 = Cl D2
let D1 be Subset of X1; for D2 being Subset of X2 st D1 = D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) holds
Cl D1 = Cl D2
let D2 be Subset of X2; ( D1 = D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) implies Cl D1 = Cl D2 )
assume A1:
D1 = D2
; ( not TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) or Cl D1 = Cl D2 )
assume A2:
TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #)
; Cl D1 = Cl D2
then reconsider C2 = Cl D1 as Subset of X2 ;
D1 c= Cl D1
by PRE_TOPC:18;
then A3:
Cl D2 c= C2
by A1, A2, Th79, TOPS_1:5;
reconsider C1 = Cl D2 as Subset of X1 by A2;
D2 c= Cl D2
by PRE_TOPC:18;
then
Cl D1 c= C1
by A1, A2, Th79, TOPS_1:5;
hence
Cl D1 = Cl D2
by A3; verum