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;

then A ` is closed by Def6;

hence A is open by TOPS_1:4; :: thesis: verum

( 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
( A = {} or A ` is finite )
; :: thesis: 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;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

then A ` is closed by Def6;

hence A is open by TOPS_1:4; :: thesis: verum