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