consider R being connected Order of A;
R in LinOrders A by Def3;
hence not LinOrders A is empty ; :: thesis: verum