let A be non degenerated commutative Ring; :: thesis: for p being Element of Spectrum A holds 1. A in Loc (A,p)
let p be Element of Spectrum A; :: thesis: 1. A in Loc (A,p)
reconsider p = p as prime Ideal of A by Lm5;
not 1. A in p by IDEAL_1:19;
hence 1. A in Loc (A,p) by XBOOLE_0:def 5; :: thesis: verum