let c1, c2 be Element of A; :: thesis: ( 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

A3: c1 <= a and

A4: c1 <= b and

A5: for c being Element of A st c <= a & c <= b holds

c <= c1 and

A6: c2 <= a and

A7: c2 <= b and

A8: for c being Element of A st c <= a & c <= b holds

c <= c2 ; :: thesis: c1 = c2

A9: c1 <= c2 by A3, A4, A8;

c2 <= c1 by A5, A6, A7;

hence c1 = c2 by A1, A9, ORDERS_2:2; :: thesis: verum

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

A3: c1 <= a and

A4: c1 <= b and

A5: for c being Element of A st c <= a & c <= b holds

c <= c1 and

A6: c2 <= a and

A7: c2 <= b and

A8: for c being Element of A st c <= a & c <= b holds

c <= c2 ; :: thesis: c1 = c2

A9: c1 <= c2 by A3, A4, A8;

c2 <= c1 by A5, A6, A7;

hence c1 = c2 by A1, A9, ORDERS_2:2; :: thesis: verum