let s, t be Element of L; :: thesis: ( ( for x being Element of L st x in A holds

x <= s ) & s in A & ( for x being Element of L st x in A holds

x <= t ) & t in A implies s = t )

assume ( ( for x being Element of L st x in A holds

x <= s ) & s in A & ( for y being Element of L st y in A holds

y <= t ) & t in A ) ; :: thesis: s = t

then ( t <= s & s <= t ) ;

hence s = t by ORDERS_2:2; :: thesis: verum

x <= s ) & s in A & ( for x being Element of L st x in A holds

x <= t ) & t in A implies s = t )

assume ( ( for x being Element of L st x in A holds

x <= s ) & s in A & ( for y being Element of L st y in A holds

y <= t ) & t in A ) ; :: thesis: s = t

then ( t <= s & s <= t ) ;

hence s = t by ORDERS_2:2; :: thesis: verum