let
p
be
integer
Number
;
:: thesis:
(
p
is
prime
implies
p
is
natural
)
assume
p
is
prime
;
:: thesis:
p
is
natural
then
p
in
NAT
by
INT_1:3
;
hence
p
is
natural
;
:: thesis:
verum