theorem :: RINGFRAC:36

for A being non degenerated commutative Ring
for p being Element of Spectrum A holds
( A ~ p is local & Loc-Ideal p is maximal Ideal of (A ~ p) )