let L be non empty reflexive antisymmetric RelStr ; :: thesis: for x, y being Element of L st x << y & x >> y holds
x = y
let x, y be Element of L; :: thesis: ( x << y & x >> y implies x = y )
assume ( x << y & x >> y ) ; :: thesis: x = y
then ( x <= y & y <= x ) by Th1;
hence x = y by ORDERS_2:25; :: thesis: verum