let Y be non empty TopSpace; :: thesis: ( ( for X being non empty TopSpace
for f being Function of X,Y holds f is continuous ) implies Y is anti-discrete )
set X = ADTS the carrier of Y;
A1: ADTS the carrier of Y = TopStruct(# the carrier of Y,(cobool the carrier of Y) #) by TEX_1:def 3;
then reconsider f = id the carrier of Y as Function of (ADTS the carrier of Y),Y ;
assume for X being non empty TopSpace
for f being Function of X,Y holds f is continuous ; :: thesis: Y is anti-discrete
then A2: f is continuous ;
for A being Subset of Y holds
( not A is closed or A = {} or A = the carrier of Y )
proof
let A be Subset of Y; :: thesis: ( not A is closed or A = {} or A = the carrier of Y )
reconsider B = A as Subset of (ADTS the carrier of Y) by A1;
A3: f " A = B by FUNCT_2:94;
assume A is closed ; :: thesis: ( A = {} or A = the carrier of Y )
then B is closed by A2, A3;
hence ( A = {} or A = the carrier of Y ) by A1, TDLAT_3:19; :: thesis: verum
end;
hence Y is anti-discrete by TDLAT_3:19; :: thesis: verum