:: deftheorem Def1 defines total ORDERS_2:def 1 :
for A being RelStr holds
( A is total iff the InternalRel of A is total );