theorem Th1: :: YELLOW_7:1

for L being RelStr
for x, y being Element of (L opp) holds
( x <= y iff ~ x >= ~ y )