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

a <_ o,b

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

a <_ o,b

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

a <_ o,b

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

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

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

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

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

a <_ o,b

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

a <_ o,b

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}[x,y]
by A1, A3;

hence [x,z] in R by A1, A4; :: 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, A4; :: thesis: verum

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

a <_ o,b

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

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

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

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