let X be non empty TopSpace; :: thesis: ( ( for Y being non empty TopSpace
for f being Function of X,Y holds f is continuous ) implies X is discrete )
set Y = 1TopSp the carrier of X;
reconsider f = id the carrier of X as Function of X,(1TopSp the carrier of X) ;
assume for Y being non empty TopSpace
for f being Function of X,Y holds f is continuous ; :: thesis: X is discrete
then A1: f is continuous ;
for A being Subset of X holds A is closed
proof
let A be Subset of X; :: thesis: A is closed
reconsider B = A as Subset of (1TopSp the carrier of X) ;
A2: f " B = A by FUNCT_2:94;
B is closed by TDLAT_3:16;
hence A is closed by A1, A2; :: thesis: verum
end;
hence X is discrete by TDLAT_3:16; :: thesis: verum