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
now :: thesis: for F being set holds
( 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;
hence T1 = T2 by Th6; :: thesis: verum