let M be non countable Aleph; :: thesis:
consider L being Sequence such that
A1: ( dom L = M & ( for A being Ordinal st A in M holds
L . A = H₁(A) ) ) from ORDINAL2:sch 2();
A2: rng L is c=-linear

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

end;

let X be set ; :: thesis:
assume X in rng L ; :: thesis:
then consider x being object such that
A12: x in dom L and
A13: X = L . x by FUNCT_1:def 3;
reconsider x = x as Ordinal by A12;
card (Rank x) in M by A11, A1, A12, Th34;
hence card X in M by A1, A12, A13; :: thesis:

end;