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