theorem Th7: :: ROBBINS3:7

for O being non empty PartialOrdered OrderInvolutive OrthoRelStr
for x, y being Element of O st x <= y holds
y ` <= x `