theorem Th8: :: ARROW:8
for A being non empty set
for b being Element of A ex o being Element of LinPreorders A st
for a being Element of A st a <> b holds
b <_ o,a