theorem Th2: :: YELLOW_7:2

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