let n be Nat; :: thesis: ( 1 < n implies n |-count n = 1 )
assume A1: 1 < n ; :: thesis: n |-count n = 1
A2: now :: thesis: not n |^ (1 + 1) divides n
assume n |^ (1 + 1) divides n ; :: thesis: contradiction
then n |^ 2 <= n by A1, NAT_D:7;
hence contradiction by A1, PREPOWER:13; :: thesis: verum
end;
n |^ 1 divides n ;
hence n |-count n = 1 by A1, A2, Def7; :: thesis: verum