theorem :: FIELD_7:2

for R, S being strict Ring holds
( R == S iff R = S ) ;