p is prime Ideal of A by Lm5;
then A1: 0. A in p by IDEAL_1:2;
A2: 1. A in Loc (A,p) by Th52;
then reconsider a = [(0. A),(1. A)] as Element of Frac (Loc (A,p)) by Def3;
A3: a in [:p,(Loc (A,p)):] by A1, A2, ZFMISC_1:87;
reconsider y = Class ((EqRel (Loc (A,p))),a) as Element of (A ~ p) by Lm41;
y in Loc-Ideal p by A3;
hence not Loc-Ideal p is empty ; :: thesis: verum