let i, j, n be Nat; :: thesis: for a being non trivial Nat st Px (a,i), Px (a,j) are_congruent_mod Px (a,n) & i < n & j < n holds
i = j
let a be non trivial Nat; :: thesis: ( Px (a,i), Px (a,j) are_congruent_mod Px (a,n) & i < n & j < n implies i = j )
assume A1: ( Px (a,i), Px (a,j) are_congruent_mod Px (a,n) & i < n & j < n ) ; :: thesis: i = j
then ( Px (a,i) < Px (a,n) & Px (a,j) < Px (a,n) ) by Th19;
then A2: Px (a,i) = Px (a,j) by Lm7, A1;
( i < j or i = j or j < i ) by XXREAL_0:1;
hence i = j by A2, Th19; :: thesis: verum