let X be non empty TopSpace; :: thesis: for Y being non empty anti-discrete TopSpace
for f being Function of X,Y holds f is continuous
let Y be non empty anti-discrete TopSpace; :: thesis: for f being Function of X,Y holds f is continuous
let f be Function of X,Y; :: thesis: f is continuous

now

let B be Subset of Y; :: thesis: ( B is closed implies f " B is closed )
assume A1: B is closed ; :: thesis: f " B is closed

now

per cases ( B = {} or B = the carrier of Y ) by A1, TDLAT_3:19;

suppose B = {} ; :: thesis: f " B is closed

then f " B = {} X by RELAT_1:136;
hence f " B is closed ; :: thesis: verum

end;

suppose B = the carrier of Y ; :: thesis: f " B is closed

then B = [#] Y ;
then f " B = [#] X by TOPS_2:41;
hence f " B is closed ; :: thesis: verum

end;

end;

end;

hence f " B is closed ; :: thesis: verum

end;

hence f is continuous by PRE_TOPC:def 6; :: thesis: verum