:: deftheorem defines Loc-Ideal RINGFRAC:def 22 :
for A being non degenerated commutative Ring
for p being Element of Spectrum A holds Loc-Ideal p = { y where y is Element of (A ~ p) : ex a being Element of Frac (Loc (A,p)) st
( a in [:p,(Loc (A,p)):] & y = Class ((EqRel (Loc (A,p))),a) ) } ;