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₁[ 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₁[x,y] ) from RELSET_1:sch 2();

A2: now

let x, y be Element of A; :: thesis: ( [x,y] in R or [y,x] in R )
A3: ( S₁[x,y] or S₁[y,x] ) ;
thus ( [x,y] in R or [y,x] in R ) by A1, A3; :: thesis: verum

end;

A4: now

let x, y, z be Element of A; :: thesis: ( [x,y] in R & [y,z] in R implies [x,z] in R )
assume that
A5: [x,y] in R and
A6: [y,z] in R ; :: thesis: [x,z] in R
A7: S₁[x,y] by A1, A5;
thus [x,z] in R by A1, A6, A7; :: thesis: verum

end;

reconsider o = R as Element of LinPreorders A by A2, A4, Def1;
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 A8: a <> b ; :: thesis: a <_ o,b
A9: not [b,a] in R by A1, A8;
thus a <_ o,b by A9, Def4; :: thesis: verum