theorem Th54: :: RINGFRAC:35

for A being non degenerated commutative Ring
for p being Element of Spectrum A
for x being object st x in ([#] (A ~ p)) \ (Loc-Ideal p) holds
x is Unit of (A ~ p)