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 A1: ( a <=_ o,b or a <_ o,b ) ; :: thesis: ( ( not b <=_ o,c & not b <_ o,c ) or a <=_ o,c )
A2: a <=_ o,b by A1, Th4;
A3: [a,b] in o by A2, Def4;
assume A4: ( b <=_ o,c or b <_ o,c ) ; :: thesis: a <=_ o,c
A5: b <=_ o,c by A4, Th4;
A6: [b,c] in o by A5, Def4;
thus [a,c] in o by A3, A6, Def1; :: according to ARROW:def 4 :: thesis: verum