let T1, T2 be strict TopSpace; :: thesis: ( the carrier of T1 = X & ( for A being Subset of T1 holds Cl A = IFEQ (A,{},A,(A \/ ({x0} /\ X))) ) & the carrier of T2 = X & ( for A being Subset of T2 holds Cl A = IFEQ (A,{},A,(A \/ ({x0} /\ X))) ) implies T1 = T2 )

assume that

A10: the carrier of T1 = X and

A11: for A being Subset of T1 holds Cl A = IFEQ (A,{},A,(A \/ ({x0} /\ X))) and

A12: the carrier of T2 = X and

A13: for A being Subset of T2 holds Cl A = IFEQ (A,{},A,(A \/ ({x0} /\ X))) ; :: thesis: T1 = T2

assume that

A10: the carrier of T1 = X and

A11: for A being Subset of T1 holds Cl A = IFEQ (A,{},A,(A \/ ({x0} /\ X))) and

A12: the carrier of T2 = X and

A13: for A being Subset of T2 holds Cl A = IFEQ (A,{},A,(A \/ ({x0} /\ X))) ; :: thesis: T1 = T2

now :: thesis: for A1 being Subset of T1

for A2 being Subset of T2 st A1 = A2 holds

Cl A1 = Cl A2

hence
T1 = T2
by A10, A12, 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

hence Cl A1 = IFEQ (A2,{},A2,(A2 \/ ({x0} /\ X))) by A11

.= Cl A2 by A13 ;

:: 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

hence Cl A1 = IFEQ (A2,{},A2,(A2 \/ ({x0} /\ X))) by A11

.= Cl A2 by A13 ;

:: thesis: verum