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