let A be non degenerated commutative Ring; :: thesis: for J1, J2 being proper Ideal of A holds
( PrimeIdeals (A,J1) = PrimeIdeals (A,J2) iff sqrt J1 = sqrt J2 )
let J1, J2 be proper Ideal of A; :: thesis: ( PrimeIdeals (A,J1) = PrimeIdeals (A,J2) iff sqrt J1 = sqrt J2 )
thus ( PrimeIdeals (A,J1) = PrimeIdeals (A,J2) implies sqrt J1 = sqrt J2 ) :: thesis: ( sqrt J1 = sqrt J2 implies PrimeIdeals (A,J1) = PrimeIdeals (A,J2) )
proof
assume A2: PrimeIdeals (A,J1) = PrimeIdeals (A,J2) ; :: thesis: sqrt J1 = sqrt J2
sqrt J1 = meet (PrimeIdeals (A,J1)) by Th28
.= sqrt J2 by Th28, A2 ;
hence sqrt J1 = sqrt J2 ; :: thesis: verum
end;
assume A3: sqrt J1 = sqrt J2 ; :: thesis: PrimeIdeals (A,J1) = PrimeIdeals (A,J2)
PrimeIdeals (A,J1) = PrimeIdeals (A,(J1 -Ideal)) by IDEAL_1:44
.= PrimeIdeals (A,(sqrt (J1 -Ideal))) by Th37
.= PrimeIdeals (A,(sqrt J1)) by IDEAL_1:44
.= PrimeIdeals (A,(sqrt (J2 -Ideal))) by A3, IDEAL_1:44
.= PrimeIdeals (A,(J2 -Ideal)) by Th37
.= PrimeIdeals (A,J2) by IDEAL_1:44 ;
hence PrimeIdeals (A,J1) = PrimeIdeals (A,J2) ; :: thesis: verum