let A be non empty set ; :: thesis: for a, b, c being Element of A
for o being Element of LinPreorders A st ( a <=_ o,b or a <_ o,b ) & ( b <=_ o,c or b <_ o,c ) holds
a <=_ o,c
let a, b, c be Element of A; :: thesis: for o being Element of LinPreorders A st ( a <=_ o,b or a <_ o,b ) & ( b <=_ o,c or b <_ o,c ) holds
a <=_ o,c
let o be Element of LinPreorders A; :: thesis: ( ( a <=_ o,b or a <_ o,b ) & ( b <=_ o,c or b <_ o,c ) implies a <=_ o,c )
assume ( a <=_ o,b or a <_ o,b ) ; :: thesis: ( ( not b <=_ o,c & not b <_ o,c ) or a <=_ o,c )
then a <=_ o,b by Th4;
then A1: [a,b] in o ;
assume ( b <=_ o,c or b <_ o,c ) ; :: thesis: a <=_ o,c
then b <=_ o,c by Th4;
then [b,c] in o ;
hence [a,c] in o by A1, Def1; :: according to ARROW:def 4 :: thesis: verum