let c1, c2 be Element of A; ( 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
and
A4:
b <= c1
and
A5:
for c being Element of A st a <= c & b <= c holds
c1 <= c
and
A6:
a <= c2
and
A7:
b <= c2
and
A8:
for c being Element of A st a <= c & b <= c holds
c2 <= c
; c1 = c2
A9:
c1 <= c2
by A5, A6, A7;
c2 <= c1
by A3, A4, A8;
hence
c1 = c2
by A1, A9, ORDERS_2:2; verum