:: deftheorem defines strongly_connected ORDERS_5:def 2 :
for A being RelStr holds
( A is strongly_connected iff the InternalRel of A is_strongly_connected_in the carrier of A );