let A be non empty set ; :: thesis: for a being Element of A
for o being Element of LinPreorders A holds a <=_ o,a
let a be Element of A; :: thesis: for o being Element of LinPreorders A holds a <=_ o,a
let o be Element of LinPreorders A; :: thesis: a <=_ o,a
thus [a,a] in o by Def1; :: according to ARROW:def 4 :: thesis: verum