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 that
A12: for x being Element of L st x in A holds
x <= s and
A13: s in A and
A14: for y being Element of L st y in A holds
y <= t and
A15: t in A ; :: thesis: s = t
consider A being non empty Chain of L such that
A16: ( ( for x being Element of L st x in A holds
x <= s ) & s in A ) and
A17: ( ( for y being Element of L st y in A holds
y <= t ) & t in A ) by A12, A13, A14, A15;
A18: t <= s by A16, A17;
s <= t by A16, A17;
hence s = t by A18, ORDERS_2:25; :: thesis: verum