let A be non empty set ; :: thesis: for a, b being Element of A
for o being Element of LinPreorders A holds
( a <=_ o,b or b <=_ o,a )
let a, b be Element of A; :: thesis: for o being Element of LinPreorders A holds
( a <=_ o,b or b <=_ o,a )
let o be Element of LinPreorders A; :: thesis: ( a <=_ o,b or b <=_ o,a )
( [a,b] in o or [b,a] in o ) by Def1;
hence ( a <=_ o,b or b <=_ o,a ) by Def4; :: thesis: verum