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();

let X, Y be set ; :: thesis:
assume X in rng L ; :: thesis:
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:
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:

end;

let X be set ; :: thesis:
assume X in rng L ; :: thesis:
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:

end;