let X be TopSpace; :: thesis: ( X is almost_discrete iff for A being Subset of X st A is open holds
A is closed )
thus ( X is almost_discrete implies for A being Subset of X st A is open holds
A is closed ) :: thesis: ( ( for A being Subset of X st A is open holds
A is closed ) implies X is almost_discrete )
proof
assume A1: X is almost_discrete ; :: thesis: for A being Subset of X st A is open holds
A is closed
now :: thesis: for A being Subset of X st A is open holds
A is closed
let A be Subset of X; :: thesis: ( A is open implies A is closed )
assume A is open ; :: thesis: A is closed
then A in the topology of X by PRE_TOPC:def 2;
then the carrier of X \ A in the topology of X by A1;
then ([#] X) \ A is open by PRE_TOPC:def 2;
hence A is closed by PRE_TOPC:def 3; :: thesis: verum
end;
hence for A being Subset of X st A is open holds
A is closed ; :: thesis: verum
end;
assume A2: for A being Subset of X st A is open holds
A is closed ; :: thesis: X is almost_discrete
now :: thesis: for A being Subset of X st A in the topology of X holds
the carrier of X \ A in the topology of X
let A be Subset of X; :: thesis: ( A in the topology of X implies the carrier of X \ A in the topology of X )
reconsider A9 = A as Subset of X ;
assume A in the topology of X ; :: thesis: the carrier of X \ A in the topology of X
then A9 is open by PRE_TOPC:def 2;
then A9 is closed by A2;
then ([#] X) \ A9 is open by PRE_TOPC:def 3;
hence the carrier of X \ A in the topology of X by PRE_TOPC:def 2; :: thesis: verum
end;
hence X is almost_discrete ; :: thesis: verum