theorem Th31: :: YELLOW_7:31

for L being RelStr holds
( L opp is lower-bounded iff L is upper-bounded )