theorem :: ORDERS_5:21

for A being RelStr
for a1, a2 being Element of A st a1 <= a2 holds
not A is empty by Th29;