let L be non empty reflexive antisymmetric RelStr ; :: thesis: for x, y being Element of st uparrow x = uparrow y holds
x = y
let x, y be Element of ; :: thesis: ( uparrow x = uparrow y implies x = y )
reconsider x' = x, y' = y as Element of ;
A1: x' <= x' ;
A2: y' <= y' ;
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: x' <= y' by A4, Th18;
x' >= y' by A5, Th18;
hence x = y by A6, ORDERS_2:25; :: thesis: verum