let A be set ; :: thesis: ( A is ordinal implies A is c=-linear )
assume A is ordinal ; :: thesis: A is c=-linear
then for x, y being set st x in A & y in A holds
x,y are_c=-comparable by ORDINAL1:15;
hence A is c=-linear by ORDINAL1:def 8; :: thesis: verum