:: deftheorem Def1 defines connected ORDERS_5:def 1 :
for A being RelStr holds
( A is connected iff the InternalRel of A is_connected_in the carrier of A );