for n being Nat
for a, b being non trivial Nat holds
( Px (a,n), Px (b,n) are_congruent_mod a - b & Py (a,n), Py (b,n) are_congruent_mod a - b )