set M = { a where a is Element of R : ex n being Element of NAT st a |^ n in I } ;
not { a where a is Element of R : ex n being Element of NAT st a |^ n in I } is empty
proof
set a = the Element of I;
the Element of I |^ 1 = the Element of I by BINOM:8;
then the Element of I in { a where a is Element of R : ex n being Element of NAT st a |^ n in I } ;
hence not { a where a is Element of R : ex n being Element of NAT st a |^ n in I } is empty ; :: thesis: verum
end;
hence not sqrt I is empty ; :: thesis: verum