:: deftheorem Def2 defines with_symmetrical_domain FUNCT_8:def 2 :
for R being Relation holds
( R is with_symmetrical_domain iff dom R is symmetrical );