let p be prime Nat; :: thesis: for a being non trivial Nat holds a |-count p <= 1
let a be non trivial Nat; :: thesis: a |-count p <= 1
a > 1 by Def0;
then ( a |-count p = 0 or a = p ) by NAT_3:24;
hence a |-count p <= 1 by Def0, NAT_3:22; :: thesis: verum