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 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
A2: now :: thesis: for x, y being Element of A holds
( [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 )
( S1[x,y] or S1[y,x] ) ;
hence
( [x,y] in R or [y,x] in R ) by A1; :: thesis: verum
end;
now :: thesis: for x, y, z being Element of A st [x,y] in R & [y,z] in R holds
[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
S1[y,z] by A1, A4;
hence [x,z] in R by A1, A3; :: thesis: verum
end;
then reconsider o = R as Element of LinPreorders A by ;
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