let A be non degenerated commutative Ring; :: thesis: for S being non empty Subset of A holds PrimeIdeals (A,(sqrt (S -Ideal))) = PrimeIdeals (A,(S -Ideal))
let S be non empty Subset of A; :: thesis: PrimeIdeals (A,(sqrt (S -Ideal))) = PrimeIdeals (A,(S -Ideal))
thus PrimeIdeals (A,(sqrt (S -Ideal))) c= PrimeIdeals (A,(S -Ideal)) :: according to XBOOLE_0:def 10 :: thesis: PrimeIdeals (A,(S -Ideal)) c= PrimeIdeals (A,(sqrt (S -Ideal)))
proof
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in PrimeIdeals (A,(sqrt (S -Ideal))) or p in PrimeIdeals (A,(S -Ideal)) )
assume p in PrimeIdeals (A,(sqrt (S -Ideal))) ; :: thesis: p in PrimeIdeals (A,(S -Ideal))
then consider p1 being prime Ideal of A such that
A3: p1 = p and
A4: sqrt (S -Ideal) c= p1 ;
S -Ideal c= p1 by A4, Th36;
hence p in PrimeIdeals (A,(S -Ideal)) by A3; :: thesis: verum
end;
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in PrimeIdeals (A,(S -Ideal)) or p in PrimeIdeals (A,(sqrt (S -Ideal))) )
assume p in PrimeIdeals (A,(S -Ideal)) ; :: thesis: p in PrimeIdeals (A,(sqrt (S -Ideal)))
then consider p1 being prime Ideal of A such that
A7: p1 = p and
A8: S -Ideal c= p1 ;
sqrt (S -Ideal) c= p1 by A8, Th35;
hence p in PrimeIdeals (A,(sqrt (S -Ideal))) by A7; :: thesis: verum