let A be non empty set ; 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; ( 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
; 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 RELSET_1:sch 2();
now for x, y, z being Element of A st [x,y] in R & [y,z] in R holds
[x,z] in Rlet x,
y,
z be
Element of
A;
( [x,y] in R & [y,z] in R implies [x,z] in R )assume
(
[x,y] in R &
[y,z] in R )
;
[x,z] in Rthen
(
S1[
x,
y] &
S1[
y,
z] )
by A3;
hence
[x,z] in R
by A3;
verum end;
then reconsider o = R as Element of LinPreorders A by A4, Def1;
take
o
; ( 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 )
; verum