:: deftheorem Def1 defines discrete ORDERS_3:def 1 :
for IT being RelStr holds
( IT is discrete iff the InternalRel of IT = id the carrier of IT );