let n, k be Nat; :: thesis: for a being non trivial Nat st Py (a,k) = Py (a,n) holds
k = n
let a be non trivial Nat; :: thesis: ( Py (a,k) = Py (a,n) implies k = n )
assume Py (a,k) = Py (a,n) ; :: thesis: k = n
then ( k >= n & n >= k ) by Th14;
hence k = n by XXREAL_0:1; :: thesis: verum