reconsider p = p as prime Ideal of A by Lm5;
0. A in p by IDEAL_1:3;
hence Loc (A,p) is without_zero by XBOOLE_0:def 5; :: thesis: verum