theorem Th30: :: YELLOW_7:30

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