let f be Ordinal-Sequence; :: thesis: ( ( for c being ordinal number st c in dom f holds
f . c = epsilon_ c ) implies f is increasing )
assume A1: for c being ordinal number st c in dom f holds
f . c = epsilon_ c ; :: thesis: f is increasing
let a be ordinal number ; :: according to ORDINAL2:def 12 :: thesis: for b₁ being set holds
( not a in b₁ or not b₁ in proj1 f or f . a in f . b₁ )
let b be ordinal number ; :: thesis: ( not a in b or not b in proj1 f or f . a in f . b )
assume A2: ( a in b & b in dom f ) ; :: thesis: f . a in f . b
then ( f . a = epsilon_ a & f . b = epsilon_ b ) by A1, ORDINAL1:10;
hence f . a in f . b by A2, Th44; :: thesis: verum