let Y, X be non empty TopSpace; :: thesis: for f being Function of X,Y holds
( f is continuous iff for x being Point of X holds f is_continuous_at x )
let f be Function of X,Y; :: thesis: ( f is continuous iff for x being Point of X holds f is_continuous_at x )
thus ( f is continuous implies for x being Point of X holds f is_continuous_at x ) :: thesis: ( ( for x being Point of X holds f is_continuous_at x ) implies f is continuous )

proof

assume A1: f is continuous ; :: thesis: for x being Point of X holds f is_continuous_at x
let x be Point of X; :: thesis: f is_continuous_at x
for G being a_neighborhood of f . x ex H being a_neighborhood of x st f .: H c= G by A1, BORSUK_1:def 3;
hence f is_continuous_at x by Def2; :: thesis: verum

end;

assume A2: for x being Point of X holds f is_continuous_at x ; :: thesis: f is continuous
thus f is continuous :: thesis: verum

proof

let x be Point of X; :: according to BORSUK_1:def 3 :: thesis: for b₁ being a_neighborhood of f . x ex b₂ being a_neighborhood of x st f .: b₂ c= b₁
let G be a_neighborhood of f . x; :: thesis: ex b₁ being a_neighborhood of x st f .: b₁ c= G
f is_continuous_at x by A2;
hence ex b₁ being a_neighborhood of x st f .: b₁ c= G by Def2; :: thesis: verum

end;