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 x' = x, y' = y as Element of L ;
A1: ( x' <= x' & y' <= y' ) ;
assume downarrow x = downarrow y ; :: thesis: x = y
then ( y in downarrow x & x in downarrow y ) by A1, Th17;
then ( x' <= y' & x' >= y' ) by Th17;
hence x = y by ORDERS_2:25; :: thesis: verum