let n be natural number ; :: thesis: ( 1 < n implies n |-count n = 1 )
assume A1: 1 < n ; :: thesis: n |-count n = 1

A2: now

assume n |^ (1 + 1) divides n ; :: thesis: contradiction
then n |^ 2 <= n by A1, NAT_D:7;
hence contradiction by A1, PREPOWER:21; :: thesis: verum

end;

n |^ 1 divides n by NEWTON:10;
hence n |-count n = 1 by A1, A2, Def7; :: thesis: verum