let A be Ordinal; :: thesis: for X being Subset of A ex s being Ordinal-Sequence st
( s is increasing & rng s = X )
let X be Subset of A; :: thesis: ex s being Ordinal-Sequence st
( s is increasing & rng s = X )
consider B being Ordinal such that
A1: RelIncl X, RelIncl B are_isomorphic by WELLORD2:8, WELLORD2:13;
consider F being Function such that
A2: F is_isomorphism_of RelIncl B, RelIncl X by A1, WELLORD1:40, WELLORD1:def 8;
field (RelIncl B) = B by WELLORD2:def 1;
then A3: dom F = B by A2, WELLORD1:def 7;
then reconsider F = F as Sequence by ORDINAL1:def 7;
A4: ( rng F = field (RelIncl X) & field (RelIncl X) = X ) by A2, WELLORD2:def 1, WELLORD1:def 7;
then reconsider F = F as Ordinal-Sequence by ORDINAL2:def 4;
take F ; :: thesis: ( F is increasing & rng F = X )

now :: thesis: for a, b being Ordinal st a in b & b in dom F holds
F . a in F . b

let a, b be Ordinal; :: thesis: ( a in b & b in dom F implies F . a in F . b )
assume A5: ( a in b & b in dom F ) ; :: thesis: F . a in F . b
A6: a c= b by A5, ORDINAL1:10;
A7: a in dom F by A5, ORDINAL1:10;
then A8: [a,b] in RelIncl B by A3, A5, A6, WELLORD2:def 1;
A9: ( F . a in X & F . b in X ) by A4, A5, A7, FUNCT_1:def 3;
a <> b by A5;
then ( [(F . a),(F . b)] in RelIncl X & F . a <> F . b ) by A8, A2, WELLORD1:36;
then F . a c< F . b by A9, WELLORD2:def 1;
hence F . a in F . b by A9, ORDINAL1:11; :: thesis: verum

end;

hence ( F is increasing & rng F = X ) by A4, ORDINAL2:def 12; :: thesis: verum