let
a
be
Nat
;
:: thesis:
for
n
being
prime
Nat
holds
(
n
divides
a
iff
n
divides
a
|^
n
)
let
n
be
prime
Nat
;
:: thesis:
(
n
divides
a
iff
n
divides
a
|^
n
)
a
divides
a
|^
n
by
NAT_3:3
;
hence
(
n
divides
a
iff
n
divides
a
|^
n
)
by
NAT_D:4
,
NAT_3:5
;
:: thesis:
verum