let f be Ordinal-Sequence; :: thesis: ( f is increasing implies f is non-decreasing )
assume A1: for a, b being Ordinal st a in b & b in dom f holds
f . a in f . b ; :: according to ORDINAL2:def 12 :: thesis: f is non-decreasing
let a be Ordinal; :: according to ORDINAL5:def 2 :: thesis: for b being Ordinal st a in b & b in dom f holds
f . a c= f . b
let b be Ordinal; :: thesis: ( a in b & b in dom f implies f . a c= f . b )
( f . a in f . b implies f . a c= f . b ) by ORDINAL1:def 2;
hence ( a in b & b in dom f implies f . a c= f . b ) by A1; :: thesis: verum