let X, Y be non empty TopSpace; :: thesis: for f being Function of X,Y st corestr f is continuous holds
f is continuous

let f be Function of X,Y; :: thesis: ( corestr f is continuous implies f is continuous )
assume A1: corestr f is continuous ; :: thesis: f is continuous
corestr f = f by WAYBEL18:def 7;
hence f is continuous by A1, PRE_TOPC:26; :: thesis: verum