let a be non zero square-containing Nat; :: thesis: a > Radical a
( Radical a <> a & Radical a <= a ) by MOEBIUS1:58;
hence a > Radical a by XXREAL_0:1; :: thesis: verum