begin
Lm1:
1 = card 1
by CARD_1:def 2;
Lm2:
2 = card 2
by CARD_1:def 2;
begin
Lm3:
for phi, psi being Ordinal-Sequence st rng phi = rng psi & phi is increasing & psi is increasing holds
for A being Ordinal st A in dom phi holds
( A in dom psi & phi . A = psi . A )
begin
begin
Lm4:
1 = card 1
by CARD_1:def 2;
begin
Lm5:
for O being Ordinal
for X being finite set st X c= O holds
order_type_of (RelIncl X) is finite