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_{1}[ 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_{1}[x,y] )
from RELSET_1:sch 2();

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

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

consider R being Relation of A such that

A3: for x, y being Element of A holds

( [x,y] in R iff S

A4: now :: thesis: for x, y being Element of A holds

( [x,y] in R or [y,x] in R )

( [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_{1}[x,y] or S_{1}[y,x] )
by A2;

hence ( [x,y] in R or [y,x] in R ) by A3; :: thesis: verum

end;( S

hence ( [x,y] in R or [y,x] in R ) by A3; :: thesis: verum

now :: thesis: for x, y, z being Element of A st [x,y] in R & [y,z] in R holds

[x,z] in R

then reconsider o = R as Element of LinPreorders A by A4, Def1;[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_{1}[x,y] & S_{1}[y,z] )
by A3;

hence [x,z] in R by A3; :: thesis: verum

end;assume ( [x,y] in R & [y,z] in R ) ; :: thesis: [x,z] in R

then ( S

hence [x,z] in R by A3; :: thesis: verum

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