:: deftheorem defines increasing ORDINAL2:def 12 :
for L being Ordinal-Sequence holds
( L is increasing iff for A, B being Ordinal st A in B & B in dom L holds
L . A in L . B );