let f be PartFunc of REAL ,REAL ; :: thesis: ( f is empty implies f is Lipschitzian )
assume Z: f is empty ; :: thesis: f is Lipschitzian
take 1 ; :: according to FCONT_1:def 3 :: thesis: ( 0 < 1 & ( for x1, x2 being real number st x1 in dom f & x2 in dom f holds
abs ((f . x1) - (f . x2)) <= 1 * (abs (x1 - x2)) ) )
thus ( 0 < 1 & ( for x1, x2 being real number st x1 in dom f & x2 in dom f holds
abs ((f . x1) - (f . x2)) <= 1 * (abs (x1 - x2)) ) ) by Z; :: thesis: verum