let A be non degenerated commutative Ring; :: thesis: for I, J being Ideal of A st sqrt I, sqrt J are_co-prime holds
I,J are_co-prime
let I, J be Ideal of A; :: thesis: ( sqrt I, sqrt J are_co-prime implies I,J are_co-prime )
assume A1: sqrt I, sqrt J are_co-prime ; :: thesis: I,J are_co-prime
sqrt (I + J) = sqrt ((sqrt I) + (sqrt J)) by Th14
.= [#] A by A1, Th13 ;
hence I,J are_co-prime by Th13; :: thesis: verum