let A be non empty set ; :: thesis:
let a, b, c be Element of A; :: thesis:
let o9 be Element of LinPreorders A; :: thesis:
assume A1: ( a <> b & a <> c ) ; :: thesis:
defpred S₁[ Element of A, Element of A] means ( $1 = a or ( $1 <=_ o9,$2 & $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 :: thesis:

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

end;

now :: thesis:

let x, y, z be Element of A; :: thesis:
assume ( [x,y] in R & [y,z] in R ) ; :: thesis:
then ( S₁[x,y] & S₁[y,z] ) by A2;
then S₁[x,z] by Th5;
hence [x,z] in R by A2; :: thesis:

end;

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