let A be non empty set ; for b being Element of A ex o being Element of LinPreorders A st
for a being Element of A st a <> b holds
a <_ o,b
let b be Element of A; ex o being Element of LinPreorders A st
for a being Element of A st a <> b holds
a <_ o,b
defpred S1[ set , set ] means ( $1 <> b or $2 = b );
consider R being Relation of A such that
A1:
for x, y being Element of A holds
( [x,y] in R iff S1[x,y] )
from RELSET_1:sch 2();
A2:
now for x, y being Element of A holds
( [x,y] in R or [y,x] in R )let x,
y be
Element of
A;
( [x,y] in R or [y,x] in R )
(
S1[
x,
y] or
S1[
y,
x] )
;
hence
(
[x,y] in R or
[y,x] in R )
by A1;
verum end;
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 that A3:
[x,y] in R
and A4:
[y,z] in R
;
[x,z] in R
S1[
x,
y]
by A1, A3;
hence
[x,z] in R
by A1, A4;
verum end;
then reconsider o = R as Element of LinPreorders A by A2, Def1;
take
o
; for a being Element of A st a <> b holds
a <_ o,b
let a be Element of A; ( a <> b implies a <_ o,b )
assume
a <> b
; a <_ o,b
then
not [b,a] in R
by A1;
hence
a <_ o,b
; verum