let A be non degenerated commutative Ring; :: thesis: for p being Element of Spectrum A holds ([#] A) \ p is multiplicatively-closed
let p be Element of Spectrum A; :: thesis: ([#] A) \ p is multiplicatively-closed
reconsider p = p as prime Ideal of A by Lm5;
reconsider M = ([#] A) \ p as Subset of A ;
A1: not 1. A in p by IDEAL_1:19;
then reconsider M = M as non empty Subset of A by XBOOLE_0:def 5;
for a, b being Element of A st a in M & b in M holds
a * b in M
proof
let a, b be Element of A; :: thesis: ( a in M & b in M implies a * b in M )
assume A2: ( a in M & b in M ) ; :: thesis: a * b in M
assume not a * b in M ; :: thesis: contradiction
then a * b in p by XBOOLE_0:def 5;
then ( a in p or b in p ) by RING_1:def 1;
hence contradiction by A2, XBOOLE_0:def 5; :: thesis: verum
end;
hence ([#] A) \ p is multiplicatively-closed by A1, XBOOLE_0:def 5; :: thesis: verum