deffunc H₃( Ordinal) -> set = Rank $1;
consider L being Sequence such that
A1: ( dom L = omega & ( for A being Ordinal st A in omega holds
L . A = H₃(A) ) ) from ORDINAL2:sch 2();

now :: thesis: for X, Y being set st X in rng L & Y in rng L holds
X,Y are_c=-comparable

let X, Y be set ; :: thesis: ( X in rng L & Y in rng L implies X,Y are_c=-comparable )
assume X in rng L ; :: thesis: ( Y in rng L implies X,Y are_c=-comparable )
then consider x being object such that
A2: x in dom L and
A3: X = L . x by FUNCT_1:def 3;
assume Y in rng L ; :: thesis: X,Y are_c=-comparable
then consider y being object such that
A4: y in dom L and
A5: Y = L . y by FUNCT_1:def 3;
reconsider x = x, y = y as Ordinal by A2, A4;
A6: Y = Rank y by A1, A4, A5;
A7: ( x c= y or y c= x ) ;
X = Rank x by A1, A2, A3;
then ( X c= Y or Y c= X ) by A6, A7, CLASSES1:37;
hence X,Y are_c=-comparable ; :: thesis: verum

end;

then A8: rng L is c=-linear ;
A9: card omega c= card (Rank omega) by CARD_1:11, CLASSES1:38;

A10: now :: thesis: for X being set st X in rng L holds
card X in card omega

let X be set ; :: thesis: ( X in rng L implies card X in card omega )
assume X in rng L ; :: thesis: card X in card omega
then consider x being object such that
A11: x in dom L and
A12: X = L . x by FUNCT_1:def 3;
reconsider x = x as Ordinal by A11;
X = Rank x by A1, A11, A12;
hence card X in card omega by A1, A11, CARD_2:67, CARD_3:42; :: thesis: verum

end;

Rank omega = Union L by A1, Lm5, Th24
.= union (rng L) by CARD_3:def 4 ;
then card (Rank omega) c= card omega by A8, A10, CARD_3:46;
hence card (Rank omega) = card omega by A9; :: thesis: verum