let o be object ; :: thesis: ( o in sqrt (sqrt I) implies o in sqrt I )
assume A1: o in sqrt (sqrt I) ; :: thesis: o in sqrt I
then reconsider o = o as Element of A ;
o in { a where a is Element of A : ex n being Element of NAT st a |^ n in sqrt I } by A1, IDEAL_1:def 24;
then consider o1 being Element of A such that
A2: o1 = o and
A3: ex n being Element of NAT st o1 |^ n in sqrt I ;
consider n1 being Element of NAT such that
A4: o1 |^ n1 in sqrt I by A3;
reconsider x = o1 |^ n1 as Element of A ;
x in { a where a is Element of A : ex n being Element of NAT st a |^ n in I } by A4, IDEAL_1:def 24;
then consider x1 being Element of A such that
A5: x1 = x and
A6: ex m being Element of NAT st x1 |^ m in I ;
consider m1 being Element of NAT such that
A7: x1 |^ m1 in I by A6;
reconsider nm = n1 * m1 as Element of NAT ;
o1 |^ nm in I by A5, A7, BINOM:11;
then o1 in { a where a is Element of A : ex n being Element of NAT st a |^ n in I } ;
hence o in sqrt I by A2, IDEAL_1:def 24; :: thesis: verum