let X0 be non empty SubSpace of X; :: thesis: X0 is almost_discrete
now :: thesis: for A0 being Subset of X0 st A0 is open holds
A0 is closed
let A0 be Subset of X0; :: thesis: ( A0 is open implies A0 is closed )
assume A0 is open ; :: thesis: A0 is closed
then consider A being Subset of X such that
A1: A is open and
A2: A0 = A /\ ([#] X0) by TOPS_2:24;
A is closed by A1, Th21;
hence A0 is closed by A2, PRE_TOPC:13; :: thesis: verum
end;
hence X0 is almost_discrete by Th21; :: thesis: verum