now :: thesis: for x, y being object st x in n -tuples_on NAT & y in n -tuples_on NAT & x <> y & not [x,y] in TuplesOrder n holds
[y,x] in TuplesOrder n

let x, y be object ; :: 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
A1: ( x in n -tuples_on NAT & y in n -tuples_on NAT ) and
x <> y and
A2: 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 A1;
not p <= q by A2, Def3;
then p > q by Th7;
then q <= p ;
hence [y,x] in TuplesOrder n by Def3; :: thesis: verum

end;

then ( field (TuplesOrder n) = n -tuples_on NAT & TuplesOrder n is_connected_in n -tuples_on NAT ) by ORDERS_1:15;
then TuplesOrder n is connected ;
hence TuplesOrder n is being_linear-order by ORDERS_1:def 6; :: thesis: verum