let n, k be Nat; :: thesis: for a being non trivial Nat st Px (a,k) = Px (a,n) holds
k = n
let a be non trivial Nat; :: thesis: ( Px (a,k) = Px (a,n) implies k = n )
( k < n or n < k or k = n ) by XXREAL_0:1;
hence ( Px (a,k) = Px (a,n) implies k = n ) by Th19; :: thesis: verum