theorem :: MOEBIUS1:58

for n being non zero Nat holds Radical n <= n by Th55, NAT_D:7;