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