let A be non empty set ; :: thesis: for a, b, c being Element of A st a <> b & b <> c & a <> c holds
ex o being Element of LinPreorders A st
( a <_ o,b & b <_ o,c )

let a, b, c be Element of A; :: thesis: ( a <> b & b <> c & a <> c implies ex o being Element of LinPreorders A st
( a <_ o,b & b <_ o,c ) )

assume that
A1: ( a <> b & b <> c ) and
A2: a <> c ; :: thesis: ex o being Element of LinPreorders A st
( a <_ o,b & b <_ o,c )

defpred S1[ set , set ] means ( ( \$1 = a or \$2 <> a ) & ( \$1 <> c or \$2 = c ) );
consider R being Relation of A such that
A3: for x, y being Element of A holds
( [x,y] in R iff S1[x,y] ) from
A4: now :: thesis: for x, y being Element of A holds
( [x,y] in R or [y,x] in R )
let x, y be Element of A; :: thesis: ( [x,y] in R or [y,x] in R )
( S1[x,y] or S1[y,x] ) by A2;
hence ( [x,y] in R or [y,x] in R ) by A3; :: thesis: verum
end;
now :: thesis: for x, y, z being Element of A st [x,y] in R & [y,z] in R holds
[x,z] in R
let x, y, z be Element of A; :: thesis: ( [x,y] in R & [y,z] in R implies [x,z] in R )
assume ( [x,y] in R & [y,z] in R ) ; :: thesis: [x,z] in R
then ( S1[x,y] & S1[y,z] ) by A3;
hence [x,z] in R by A3; :: thesis: verum
end;
then reconsider o = R as Element of LinPreorders A by ;
take o ; :: thesis: ( a <_ o,b & b <_ o,c )
( not [b,a] in R & not [c,b] in R ) by A1, A3;
hence ( a <_ o,b & b <_ o,c ) ; :: thesis: verum