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

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