let X be set ; :: thesis: for A being Subset of (ClFinTop X) holds
( A is open iff ( A = {} or A ` is finite ) )
let A be Subset of (ClFinTop X); :: thesis: ( A is open iff ( A = {} or A ` is finite ) )
A1: the carrier of (ClFinTop X) = X by Def6;
hereby :: thesis: ( ( A = {} or A ` is finite ) implies A is open )
assume that
A2: A is open and
A3: A <> {} ; :: thesis: A ` is finite
(A `) ` = A ;
then A ` <> [#] the carrier of (ClFinTop X) by A3, XBOOLE_1:37;
hence A ` is finite by A2, A1, Def6; :: thesis: verum
end;
assume ( A = {} or A ` is finite ) ; :: thesis: A is open
then A ` is closed by Def6;
hence A is open by TOPS_1:4; :: thesis: verum