:: deftheorem defines strongly_connected RELAT_2:def 15 :
for R being Relation holds
( R is strongly_connected iff R is_strongly_connected_in field R );