A1: field (TuplesOrder n) = n -tuples_on NAT by ORDERS_1:100;

now

let x, y be set ; :: thesis: ( x in n -tuples_on NAT & y in n -tuples_on NAT & x <> y & not [x,y] in TuplesOrder n implies [y,x] in TuplesOrder n )
assume that
A2: x in n -tuples_on NAT and
A3: y in n -tuples_on NAT and
x <> y and
A4: not [x,y] in TuplesOrder n ; :: thesis: [y,x] in TuplesOrder n
reconsider p = x, q = y as Element of n -tuples_on NAT by A2, A3;
not p <= q by A4, Def3;
then p > q by Th7;
then q <= p by Def2;
hence [y,x] in TuplesOrder n by Def3; :: thesis: verum

end;

then TuplesOrder n is_connected_in n -tuples_on NAT by RELAT_2:def 6;
then TuplesOrder n is connected by A1, RELAT_2:def 14;
hence TuplesOrder n is being_linear-order by ORDERS_1:def 5; :: thesis: verum