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 & rng (id A) = A ) by RELAT_1:71;
then reconsider xi = id A as T-Sequence by ORDINAL1:def 7;
reconsider xi = xi as Ordinal-Sequence by A1, Def8;
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:71; :: thesis: ( xi is increasing & A = sup xi )
thus xi is increasing :: thesis: A = sup xi

proof

let B be Ordinal; :: according to ORDINAL2:def 16 :: 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 A2: ( B in C & C in dom xi ) ; :: thesis: xi . B in xi . C
then ( B in dom xi & xi . C = C ) by A1, FUNCT_1:35, ORDINAL1:19;
hence xi . B in xi . C by A1, A2, FUNCT_1:35; :: thesis: verum

end;

thus A = sup xi by A1, Th26; :: thesis: verum