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 S₁[ 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 S₁[x,y] ) from RELSET_1:sch 2();

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 )
( S₁[x,y] or S₁[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 ( S₁[x,y] & S₁[y,z] ) by A3;
hence [x,z] in R by A3; :: thesis: verum

end;

then reconsider o = R as Element of LinPreorders A by A4, Def1;
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