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