theorem Th7: :: YELLOW_0:7

for L being RelStr
for a, b being Element of L holds
( ( a is_<=_than {b} implies a <= b ) & ( a <= b implies a is_<=_than {b} ) & ( a is_>=_than {b} implies b <= a ) & ( b <= a implies a is_>=_than {b} ) )