let A, B, C be Ordinal; :: thesis: ( A is_cofinal_with B & B is_cofinal_with C implies A is_cofinal_with C )
given xi1 being Ordinal-Sequence such that A1: ( dom xi1 = B & rng xi1 c= A & xi1 is increasing & A = sup xi1 ) ; :: according to ORDINAL2:def 21 :: thesis: ( not B is_cofinal_with C or A is_cofinal_with C )
given xi2 being Ordinal-Sequence such that A2: ( dom xi2 = C & rng xi2 c= B & xi2 is increasing & B = sup xi2 ) ; :: according to ORDINAL2:def 21 :: thesis: A is_cofinal_with C
consider xi being Ordinal-Sequence such that
A3: ( xi = xi1 * xi2 & xi is increasing ) by A1, A2, Th13;
take xi ; :: according to ORDINAL2:def 21 :: thesis: ( dom xi = C & rng xi c= A & xi is increasing & A = sup xi )
thus A4: dom xi = C by A1, A2, A3, RELAT_1:46; :: thesis: ( rng xi c= A & xi is increasing & A = sup xi )
rng xi c= rng xi1 by A3, RELAT_1:45;
hence ( rng xi c= A & xi is increasing ) by A1, A3, XBOOLE_1:1; :: thesis: A = sup xi
then A5: ( sup xi = sup (rng xi) & sup xi1 = sup (rng xi1) & sup xi2 = sup (rng xi2) & sup (rng xi) c= sup A & sup A = A ) by ORDINAL2:26, ORDINAL2:30;
thus A c= sup xi :: according to XBOOLE_0:def 10 :: thesis: sup xi c= A

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in A or a in sup xi )
assume A6: a in A ; :: thesis: a in sup xi
then reconsider a = a as Ordinal ;
consider b being Ordinal such that
A7: ( b in rng xi1 & a c= b ) by A1, A6, ORDINAL2:29;
consider e being set such that
A8: ( e in B & b = xi1 . e ) by A1, A7, FUNCT_1:def 5;
reconsider e = e as Ordinal by A8;
consider c being Ordinal such that
A9: ( c in rng xi2 & e c= c ) by A2, A8, ORDINAL2:29;
consider u being set such that
A10: ( u in C & c = xi2 . u ) by A2, A9, FUNCT_1:def 5;
reconsider u = u as Ordinal by A10;
( xi1 . e c= xi1 . c & xi1 . c = xi . u & xi . u in rng xi & xi . u is Ordinal ) by A1, A2, A3, A4, A9, A10, Th9, FUNCT_1:22, FUNCT_1:def 5;
then ( xi . u in sup xi & xi . u is Ordinal & a c= xi . u ) by A7, A8, ORDINAL2:27, XBOOLE_1:1;
hence a in sup xi by ORDINAL1:22; :: thesis: verum

end;

thus sup xi c= A by A5; :: thesis: verum