let A, B, C be Ordinal; ( 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
; ORDINAL2:def 17 ( 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
; ORDINAL2:def 17 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
; ORDINAL2:def 17 ( 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; ( 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; A = sup xi
thus
A c= sup xi
XBOOLE_0:def 10 sup xi c= Aproof
let a be
object ;
TARSKI:def 3 ( not a in A or a in sup xi )
assume A13:
a in A
;
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;
verum
end;
sup (rng xi) c= sup A
by A12, ORDINAL2:22;
hence
sup xi c= A
by ORDINAL2:18; verum