let A be non empty set ; :: thesis: 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
( b <_ o,a & c <_ o,a & ( 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 ) )
let a, b, c be Element of A; :: thesis: for o9 being Element of LinPreorders A st a <> b & a <> c holds
ex o being Element of LinPreorders A st
( b <_ o,a & c <_ o,a & ( 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 ) )
let o9 be Element of LinPreorders A; :: thesis: ( a <> b & a <> c implies ex o being Element of LinPreorders A st
( b <_ o,a & c <_ o,a & ( 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 ) ) )
assume A1: ( a <> b & a <> c ) ; :: thesis: ex o being Element of LinPreorders A st
( b <_ o,a & c <_ o,a & ( 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 ) )
defpred S₁[ Element of A, Element of A] means ( ( $1 <> a & $1 <=_ o9,$2 ) or $2 = a );
consider R being Relation of A such that
A2: for x, y being Element of A holds
( [x,y] in R iff S₁[x,y] ) from RELSET_1:sch 2();

A3: now

let x, y be Element of A; :: thesis: ( [x,y] in R or [y,x] in R )
A4: ( S₁[x,y] or S₁[y,x] ) by Th4;
thus ( [x,y] in R or [y,x] in R ) by A2, A4; :: thesis: verum

end;

A5: now

let x, y, z be Element of A; :: thesis: ( [x,y] in R & [y,z] in R implies [x,z] in R )
assume A6: ( [x,y] in R & [y,z] in R ) ; :: thesis: [x,z] in R
A7: ( S₁[x,y] & S₁[y,z] ) by A2, A6;
A8: S₁[x,z] by A7, Th5;
thus [x,z] in R by A2, A8; :: thesis: verum

end;

reconsider o = R as Element of LinPreorders A by A3, A5, Def1;
take o ; :: thesis: ( b <_ o,a & c <_ o,a & ( 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 ) )
A9: ( not [a,b] in R & not [a,c] in R ) by A1, A2;
A10: ( not [c,b] in R iff b <_ o9,c ) by A1, A2;
A11: ( not [b,c] in R iff c <_ o9,b ) by A1, A2;
thus ( b <_ o,a & c <_ o,a & ( 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 ) ) by A9, A10, A11, Def4; :: thesis: verum