let A be non degenerated commutative Ring; 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; PrimeIdeals (A,(sqrt (S -Ideal))) = PrimeIdeals (A,(S -Ideal))
thus
PrimeIdeals (A,(sqrt (S -Ideal))) c= PrimeIdeals (A,(S -Ideal))
XBOOLE_0:def 10 PrimeIdeals (A,(S -Ideal)) c= PrimeIdeals (A,(sqrt (S -Ideal)))
let p be object ; TARSKI:def 3 ( not p in PrimeIdeals (A,(S -Ideal)) or p in PrimeIdeals (A,(sqrt (S -Ideal))) )
assume
p in PrimeIdeals (A,(S -Ideal))
; 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; verum