:: deftheorem defines disconnected ORDERS_3:def 3 :
for IT being RelStr holds
( IT is disconnected iff [#] IT is disconnected );