(<=> (Commutative-Ring ?Domain ?Plus-Op ?Zero-Id ?Mult-Op ?One-Id) (And (Abelian-Group ?Domain ?Plus-Op ?Zero-Id) (Abelian-Semigroup ?Domain ?Mult-Op ?One-Id) (Distributes ?Mult-Op ?Plus-Op ?Domain)))
(<=> (Commutative-Ring ?Domain ?Plus-Op ?Zero-Id ?Mult-Op ?One-Id) (And (Abelian-Group ?Domain ?Plus-Op ?Zero-Id) (Abelian-Semigroup ?Domain ?Mult-Op ?One-Id) (Distributes ?Mult-Op ?Plus-Op ?Domain))) (Subrelation-Of Integral-Domain Commutative-Ring) (<=> (Integral-Domain ?Domain ?Plus-Op ?Zero-Id ?Mult-Op ?One-Id) (And (Commutative-Ring ?Domain ?Plus-Op ?Zero-Id ?Mult-Op ?One-Id) (Binary-Operator-On ?Mult-Op (Kappa (?X) (And (Instance-Of ?X ?Domain) (/= ?X ?Zero-Id))))))