:: deftheorem defines continuous FUZIMPL3:def 7 :
for f being UnOp of [.0,1.] holds
( f is continuous iff ex g being Function of I[01],I[01] st
( f = g & g is continuous ) );