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