:: deftheorem defines connected RELAT_2:def 14 :
for R being Relation holds
( R is connected iff R is_connected_in field R );