theorem Th29: :: ORDERS_5:20

for A being RelStr
for a1, a2 being Element of A st a1 <= a2 holds
( a1 in the carrier of A & a2 in the carrier of A )