:: deftheorem defines Loc RINGFRAC:def 20 :
for A being non degenerated commutative Ring
for p being Element of Spectrum A holds Loc (A,p) = ([#] A) \ p;