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