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 and

A2: rng xi1 c= A and

A3: xi1 is increasing and

A4: A = sup xi1 ; :: according to ORDINAL2:def 17 :: thesis: ( not B is_cofinal_with C or A is_cofinal_with C )

given xi2 being Ordinal-Sequence such that A5: dom xi2 = C and

A6: rng xi2 c= B and

A7: xi2 is increasing and

A8: B = sup xi2 ; :: according to ORDINAL2:def 17 :: thesis: A is_cofinal_with C

consider xi being Ordinal-Sequence such that

A9: xi = xi1 * xi2 and

A10: xi is increasing by A3, A7, Th13;

take xi ; :: according to ORDINAL2:def 17 :: thesis: ( dom xi = C & rng xi c= A & xi is increasing & A = sup xi )

thus A11: dom xi = C by A1, A5, A6, A9, RELAT_1:27; :: thesis: ( rng xi c= A & xi is increasing & A = sup xi )

rng xi c= rng xi1 by A9, RELAT_1:26;

hence A12: ( rng xi c= A & xi is increasing ) by A2, A10; :: thesis: A = sup xi

thus A c= sup xi :: according to XBOOLE_0:def 10 :: thesis: sup xi c= A

hence sup xi c= A by ORDINAL2:18; :: thesis: verum

given xi1 being Ordinal-Sequence such that A1: dom xi1 = B and

A2: rng xi1 c= A and

A3: xi1 is increasing and

A4: A = sup xi1 ; :: according to ORDINAL2:def 17 :: thesis: ( not B is_cofinal_with C or A is_cofinal_with C )

given xi2 being Ordinal-Sequence such that A5: dom xi2 = C and

A6: rng xi2 c= B and

A7: xi2 is increasing and

A8: B = sup xi2 ; :: according to ORDINAL2:def 17 :: thesis: A is_cofinal_with C

consider xi being Ordinal-Sequence such that

A9: xi = xi1 * xi2 and

A10: xi is increasing by A3, A7, Th13;

take xi ; :: according to ORDINAL2:def 17 :: thesis: ( dom xi = C & rng xi c= A & xi is increasing & A = sup xi )

thus A11: dom xi = C by A1, A5, A6, A9, RELAT_1:27; :: thesis: ( rng xi c= A & xi is increasing & A = sup xi )

rng xi c= rng xi1 by A9, RELAT_1:26;

hence A12: ( rng xi c= A & xi is increasing ) by A2, A10; :: thesis: A = sup xi

thus A c= sup xi :: according to XBOOLE_0:def 10 :: thesis: sup xi c= A

proof

sup (rng xi) c= sup A
by A12, ORDINAL2:22;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in A or a in sup xi )

assume A13: a in A ; :: thesis: a in sup xi

then reconsider a = a as Ordinal ;

consider b being Ordinal such that

A14: b in rng xi1 and

A15: a c= b by A4, A13, ORDINAL2:21;

consider e being object such that

A16: e in B and

A17: b = xi1 . e by A1, A14, FUNCT_1:def 3;

reconsider e = e as Ordinal by A16;

consider c being Ordinal such that

A18: c in rng xi2 and

A19: e c= c by A8, A16, ORDINAL2:21;

consider u being object such that

A20: u in C and

A21: c = xi2 . u by A5, A18, FUNCT_1:def 3;

reconsider u = u as Ordinal by A20;

A22: xi1 . c = xi . u by A9, A11, A20, A21, FUNCT_1:12;

xi . u in rng xi by A11, A20, FUNCT_1:def 3;

then A23: xi . u in sup xi by ORDINAL2:19;

xi1 . e c= xi1 . c by A1, A3, A6, A18, A19, Th9;

hence a in sup xi by A15, A17, A22, A23, ORDINAL1:12, XBOOLE_1:1; :: thesis: verum

end;assume A13: a in A ; :: thesis: a in sup xi

then reconsider a = a as Ordinal ;

consider b being Ordinal such that

A14: b in rng xi1 and

A15: a c= b by A4, A13, ORDINAL2:21;

consider e being object such that

A16: e in B and

A17: b = xi1 . e by A1, A14, FUNCT_1:def 3;

reconsider e = e as Ordinal by A16;

consider c being Ordinal such that

A18: c in rng xi2 and

A19: e c= c by A8, A16, ORDINAL2:21;

consider u being object such that

A20: u in C and

A21: c = xi2 . u by A5, A18, FUNCT_1:def 3;

reconsider u = u as Ordinal by A20;

A22: xi1 . c = xi . u by A9, A11, A20, A21, FUNCT_1:12;

xi . u in rng xi by A11, A20, FUNCT_1:def 3;

then A23: xi . u in sup xi by ORDINAL2:19;

xi1 . e c= xi1 . c by A1, A3, A6, A18, A19, Th9;

hence a in sup xi by A15, A17, A22, A23, ORDINAL1:12, XBOOLE_1:1; :: thesis: verum

hence sup xi c= A by ORDINAL2:18; :: thesis: verum