:: deftheorem Def3 defines Subring C0SP1:def 3 :
for V, b₂ being Ring holds
( b₂ is Subring of V iff ( the carrier of b₂ c= the carrier of V & the addF of b₂ = the addF of V || the carrier of b₂ & the multF of b₂ = the multF of V || the carrier of b₂ & 1. b₂ = 1. V & 0. b₂ = 0. V ) );