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