theorem Th10: :: ARROW:10

for A being non empty set
for a, b, c being Element of A
for o9 being Element of LinPreorders A st a <> b & a <> c holds
ex o being Element of LinPreorders A st
( a <_ o,b & a <_ o,c & ( b <_ o,c implies b <_ o9,c ) & ( b <_ o9,c implies b <_ o,c ) & ( c <_ o,b implies c <_ o9,b ) & ( c <_ o9,b implies c <_ o,b ) )