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 that
A1: x << y and
A2: x >> y ; :: thesis: x = y
A3: x <= y by A1, Th1;
y <= x by A2, Th1;
hence x = y by A3, ORDERS_2:2; :: thesis: verum