:: deftheorem defines normal ORDINAL6:def 3 :
for f being Ordinal-Sequence holds
( f is normal iff ( f is increasing & f is continuous ) );