:: deftheorem defines are_disjoint FIELD_2:def 1 :
for R, S being Ring holds
( R,S are_disjoint iff ([#] R) /\ ([#] S) = {} );