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