:: deftheorem Def11 defines symmetric RELAT_2:def 11 :
for R being Relation holds
( R is symmetric iff R is_symmetric_in field R );