:: deftheorem defines continuous ORDINAL2:def 13 :
for L being Ordinal-Sequence holds
( L is continuous iff for A, B being Ordinal st A in dom L & A <> 0 & A is limit_ordinal & B = L . A holds
B is_limes_of L | A );