theorem Th3: :: ARROW:3

for A being non empty set
for a being Element of A
for o being Element of LinPreorders A holds a <=_ o,a by Def1;