theorem Th4: :: ARROW:4

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