let A be Ordinal; :: thesis: ex xi being Ordinal-Sequence st
( dom xi = A & rng xi c= A & xi is increasing & A = sup xi )
A1: dom (id A) = A by RELAT_1:45;
then reconsider xi = id A as Sequence by ORDINAL1:def 7;
A2: rng (id A) = A by RELAT_1:45;
then reconsider xi = xi as Ordinal-Sequence by Def4;
take xi ; :: thesis: ( dom xi = A & rng xi c= A & xi is increasing & A = sup xi )
thus ( dom xi = A & rng xi c= A ) by RELAT_1:45; :: thesis: ( xi is increasing & A = sup xi )
thus xi is increasing :: thesis: A = sup xi
proof
let B be Ordinal; :: according to ORDINAL2:def 12 :: thesis: for B being Ordinal st B in B & B in dom xi holds
xi . B in xi . B
let C be Ordinal; :: thesis: ( B in C & C in dom xi implies xi . B in xi . C )
assume that
A3: B in C and
A4: C in dom xi ; :: thesis: xi . B in xi . C
xi . C = C by A1, A4, FUNCT_1:18;
hence xi . B in xi . C by A1, A3, A4, FUNCT_1:18, ORDINAL1:10; :: thesis: verum
end;
thus A = sup xi by A2, Th18; :: thesis: verum