consider m being Integer, k being Element of NAT such that
A1: k <> 0 and
A2: p = m / k and
A3: for n being Integer
for l being Element of NAT st l <> 0 & p = n / l holds
k <= l by Th25;
take k ; :: thesis: ( k <> 0 & ex m being Integer st p = m / k & ( for n being Integer
for k being Element of 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 Element of NAT st k <> 0 & p = n / k holds
k <= k ) ) by A1, A2, A3; :: thesis: verum