let X be non empty set ; :: thesis: for P being Subset of (CofinTop X) holds

( P is closed iff ( P = X or P is finite ) )

let P be Subset of (CofinTop X); :: thesis: ( P is closed iff ( P = X or P is finite ) )

set T = CofinTop X;

the carrier of (CofinTop X) = X by Def6;

then ( P in {X} or P in Fin X ) by A4, FINSUB_1:def 5, TARSKI:def 1;

then P in {X} \/ (Fin X) by XBOOLE_0:def 3;

then P in COMPLEMENT the topology of (CofinTop X) by Def6;

then P ` in the topology of (CofinTop X) by SETFAM_1:def 7;

then P ` is open ;

hence P is closed ; :: thesis: verum

( P is closed iff ( P = X or P is finite ) )

let P be Subset of (CofinTop X); :: thesis: ( P is closed iff ( P = X or P is finite ) )

set T = CofinTop X;

hereby :: thesis: ( ( P = X or P is finite ) implies P is closed )

assume A4:
( P = X or P is finite )
; :: thesis: P is closed assume that

A1: P is closed and

A2: P <> X ; :: thesis: P is finite

P ` in the topology of (CofinTop X) by A1, PRE_TOPC:def 2;

then P in COMPLEMENT the topology of (CofinTop X) by SETFAM_1:def 7;

then A3: P in {X} \/ (Fin X) by Def6;

not P in {X} by A2, TARSKI:def 1;

then P in Fin X by A3, XBOOLE_0:def 3;

hence P is finite ; :: thesis: verum

end;A1: P is closed and

A2: P <> X ; :: thesis: P is finite

P ` in the topology of (CofinTop X) by A1, PRE_TOPC:def 2;

then P in COMPLEMENT the topology of (CofinTop X) by SETFAM_1:def 7;

then A3: P in {X} \/ (Fin X) by Def6;

not P in {X} by A2, TARSKI:def 1;

then P in Fin X by A3, XBOOLE_0:def 3;

hence P is finite ; :: thesis: verum

the carrier of (CofinTop X) = X by Def6;

then ( P in {X} or P in Fin X ) by A4, FINSUB_1:def 5, TARSKI:def 1;

then P in {X} \/ (Fin X) by XBOOLE_0:def 3;

then P in COMPLEMENT the topology of (CofinTop X) by Def6;

then P ` in the topology of (CofinTop X) by SETFAM_1:def 7;

then P ` is open ;

hence P is closed ; :: thesis: verum