let A be non empty set ; :: thesis: for b being Element of A ex o being Element of LinPreorders A st

for a being Element of A st a <> b holds

b <_ o,a

let b be Element of A; :: thesis: ex o being Element of LinPreorders A st

for a being Element of A st a <> b holds

b <_ o,a

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

take o ; :: thesis: for a being Element of A st a <> b holds

b <_ o,a

let a be Element of A; :: thesis: ( a <> b implies b <_ o,a )

assume a <> b ; :: thesis: b <_ o,a

then not [a,b] in R by A1;

hence b <_ o,a ; :: thesis: verum

for a being Element of A st a <> b holds

b <_ o,a

let b be Element of A; :: thesis: ex o being Element of LinPreorders A st

for a being Element of A st a <> b holds

b <_ o,a

defpred S

consider R being Relation of A such that

A1: for x, y being Element of A holds

( [x,y] in R iff S

A2: 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] )
;

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

end;( S

hence ( [x,y] in R or [y,x] in R ) by A1; :: 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 A2, 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 that

A3: [x,y] in R and

A4: [y,z] in R ; :: thesis: [x,z] in R

S_{1}[y,z]
by A1, A4;

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

end;assume that

A3: [x,y] in R and

A4: [y,z] in R ; :: thesis: [x,z] in R

S

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

take o ; :: thesis: for a being Element of A st a <> b holds

b <_ o,a

let a be Element of A; :: thesis: ( a <> b implies b <_ o,a )

assume a <> b ; :: thesis: b <_ o,a

then not [a,b] in R by A1;

hence b <_ o,a ; :: thesis: verum