theorem Th9: :: LATTICE3:9

for A being RelStr
for a, b being Element of A holds
( a <= b iff b ~ <= a ~ ) by RELAT_1:def 7;