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 x9 = x, y9 = y as Element of L ;

A1: x9 <= x9 ;

A2: y9 <= y9 ;

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: x9 <= y9 by A4, Th18;

x9 >= y9 by A5, Th18;

hence x = y by A6, ORDERS_2:2; :: thesis: verum

x = y

let x, y be Element of L; :: thesis: ( uparrow x = uparrow y implies x = y )

reconsider x9 = x, y9 = y as Element of L ;

A1: x9 <= x9 ;

A2: y9 <= y9 ;

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: x9 <= y9 by A4, Th18;

x9 >= y9 by A5, Th18;

hence x = y by A6, ORDERS_2:2; :: thesis: verum