:: deftheorem Def2 defines continuous FCONT_1:def 2 :
for f being PartFunc of REAL,REAL holds
( f is continuous iff for x0 being Real st x0 in dom f holds
f is_continuous_in x0 );