let k, l be Nat; ( k <> 0 & ex m being Integer st p = m / k & ( for n being Integer
for k being Nat st k <> 0 & p = n / k holds
k <= k ) & l <> 0 & ex m being Integer st p = m / l & ( for n being Integer
for k being Nat st k <> 0 & p = n / k holds
l <= k ) implies k = l )
assume that
A4:
k <> 0
and
A5:
ex m being Integer st p = m / k
and
A6:
for m1 being Integer
for k1 being Nat st k1 <> 0 & p = m1 / k1 holds
k <= k1
and
A7:
l <> 0
and
A8:
ex n being Integer st p = n / l
and
A9:
for n1 being Integer
for k1 being Nat st k1 <> 0 & p = n1 / k1 holds
l <= k1
; k = l
A10:
l <= k
by A4, A5, A9;
k <= l
by A6, A7, A8;
hence
k = l
by A10, XXREAL_0:1; verum