let L be non empty reflexive antisymmetric RelStr ; :: thesis: for x, y being Element of L st uparrow x = uparrow y holds
x = y
let x, y be Element of L; :: thesis: ( uparrow x = uparrow y implies x = y )
reconsider x9 = x, y9 = y as Element of L ;
A1: x9 <= x9 ;
A2: y9 <= y9 ;
assume A3: uparrow x = uparrow y ; :: thesis: x = y
then A4: y in uparrow x by A2, Th18;
A5: x in uparrow y by A1, A3, Th18;
A6: x9 <= y9 by A4, Th18;
x9 >= y9 by A5, Th18;
hence x = y by A6, ORDERS_2:2; :: thesis: verum