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;
hereby :: thesis: ( ( P = X or P is finite ) implies 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;
assume A4: ( P = X or P is finite ) ; :: thesis: P is closed
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