set R = the connected Order of A;
the connected Order of A in LinOrders A by Def3;
hence not LinOrders A is empty ; :: thesis: verum