:: deftheorem Def7 defines strongly_connected ORDERS_2:def 7 :
for A being RelStr
for IT being Subset of A holds
( IT is strongly_connected iff the InternalRel of A is_strongly_connected_in IT );