let T1, T2 be strict TopSpace; :: thesis: ( the carrier of T1 = X & ( for F being Subset of T1 holds

( F is closed iff ( F is finite or F = X ) ) ) & the carrier of T2 = X & ( for F being Subset of T2 holds

( F is closed iff ( F is finite or F = X ) ) ) implies T1 = T2 )

assume that

A14: the carrier of T1 = X and

A15: for F being Subset of T1 holds

( F is closed iff ( F is finite or F = X ) ) and

A16: the carrier of T2 = X and

A17: for F being Subset of T2 holds

( F is closed iff ( F is finite or F = X ) ) ; :: thesis: T1 = T2

( F is closed iff ( F is finite or F = X ) ) ) & the carrier of T2 = X & ( for F being Subset of T2 holds

( F is closed iff ( F is finite or F = X ) ) ) implies T1 = T2 )

assume that

A14: the carrier of T1 = X and

A15: for F being Subset of T1 holds

( F is closed iff ( F is finite or F = X ) ) and

A16: the carrier of T2 = X and

A17: for F being Subset of T2 holds

( F is closed iff ( F is finite or F = X ) ) ; :: thesis: T1 = T2

now :: thesis: for F being set holds

( F is closed Subset of T1 iff F is closed Subset of T2 )

hence
T1 = T2
by Th6; :: thesis: verum( F is closed Subset of T1 iff F is closed Subset of T2 )

let F be set ; :: thesis: ( F is closed Subset of T1 iff F is closed Subset of T2 )

( F is closed Subset of T1 iff ( F c= X & ( F is finite or F = X ) ) ) by A14, A15;

hence ( F is closed Subset of T1 iff F is closed Subset of T2 ) by A16, A17; :: thesis: verum

end;( F is closed Subset of T1 iff ( F c= X & ( F is finite or F = X ) ) ) by A14, A15;

hence ( F is closed Subset of T1 iff F is closed Subset of T2 ) by A16, A17; :: thesis: verum