let c1, c2 be Element of A; :: thesis: ( a <= c1 & b <= c1 & ( for c being Element of A st a <= c & b <= c holds
c1 <= c ) & a <= c2 & b <= c2 & ( for c being Element of A st a <= c & b <= c holds
c2 <= c ) implies c1 = c2 )
assume that
A3: ( a <= c1 & b <= c1 & ( for c being Element of A st a <= c & b <= c holds
c1 <= c ) ) and
A4: ( a <= c2 & b <= c2 & ( for c being Element of A st a <= c & b <= c holds
c2 <= c ) ) ; :: thesis: c1 = c2
( c1 <= c2 & c2 <= c1 ) by A3, A4;
hence c1 = c2 by A1, ORDERS_2:25; :: thesis: verum