:: deftheorem Def5 defines continuous NFCONT_4:def 5 :
for n being Element of NAT
for f being PartFunc of REAL,(REAL n) holds
( f is continuous iff for x0 being Real st x0 in dom f holds
f is_continuous_in x0 );