let T1, T2 be strict TopSpace; :: thesis: ( the carrier of T1 = X & ( for A being Subset of T1 holds Int A = IFEQ A,X,A,(A /\ X0) ) & the carrier of T2 = X & ( for A being Subset of T2 holds Int A = IFEQ A,X,A,(A /\ X0) ) implies T1 = T2 )
assume that
A9: the carrier of T1 = X and
A10: for A being Subset of T1 holds Int A = IFEQ A,X,A,(A /\ X0) and
A11: the carrier of T2 = X and
A12: for A being Subset of T2 holds Int A = IFEQ A,X,A,(A /\ X0) ; :: thesis: T1 = T2

now

let A1 be Subset of T1; :: thesis: for A2 being Subset of T2 st A1 = A2 holds
Int A1 = Int A2
let A2 be Subset of T2; :: thesis: ( A1 = A2 implies Int A1 = Int A2 )
assume A1 = A2 ; :: thesis: Int A1 = Int A2
hence Int A1 = IFEQ A2,X,A2,(A2 /\ X0) by A10
.= Int A2 by A12 ;
:: thesis: verum

end;

hence T1 = T2 by A9, A11, Th10; :: thesis: verum