consider m being Integer, k being Nat such that
A1:
k <> 0
and
A2:
p = m / k
and
A3:
for n being Integer
for l being Nat st l <> 0 & p = n / l holds
k <= l
by Th6;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
take
k
; ( 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 ) )
thus
( 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 ) )
by A1, A2, A3; verum