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