let A be non empty set ; :: thesis: for a, b being Element of A
for o'' being Element of LinOrders A st a <=_ o'',b & b <=_ o'',a holds
a = b
let a, b be Element of A; :: thesis: for o'' being Element of LinOrders A st a <=_ o'',b & b <=_ o'',a holds
a = b
let o'' be Element of LinOrders A; :: thesis: ( a <=_ o'',b & b <=_ o'',a implies a = b )
( [a,b] in o'' & [b,a] in o'' implies a = b ) by Def2;
hence ( a <=_ o'',b & b <=_ o'',a implies a = b ) by Def4; :: thesis: verum