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 )
assume A1: for Y being non empty TopSpace
for f being Function of X,Y holds f is continuous ; :: thesis: 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) ;
A2: f is continuous by A1;
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) ;
A3: B is closed by TDLAT_3:18;
f " B = A by FUNCT_2:171;
hence A is closed by A2, A3, PRE_TOPC:def 12; :: thesis: verum

end;

hence X is discrete by TDLAT_3:18; :: thesis: verum