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