for n being Nat
for a, b being non trivial Nat st a <= b holds
( Px (a,n) <= Px (b,n) & Py (a,n) <= Py (b,n) )