let x, y be Element of [:L,L:]; :: according to ORDERS_3:def 5 :: thesis: ( not x <= y or for b_{1}, b_{2} being Element of the carrier of L holds

( not b_{1} = (sup_op L) . x or not b_{2} = (sup_op L) . y or b_{1} <= b_{2} ) )

set f = sup_op L;

assume x <= y ; :: thesis: for b_{1}, b_{2} being Element of the carrier of L holds

( not b_{1} = (sup_op L) . x or not b_{2} = (sup_op L) . y or b_{1} <= b_{2} )

then A1: ( x `1 <= y `1 & x `2 <= y `2 ) by YELLOW_3:12;

A2: ( (sup_op L) . x = (x `1) "\/" (x `2) & (sup_op L) . y = (y `1) "\/" (y `2) ) by Th34;

let a, b be Element of L; :: thesis: ( not a = (sup_op L) . x or not b = (sup_op L) . y or a <= b )

assume ( a = (sup_op L) . x & b = (sup_op L) . y ) ; :: thesis: a <= b

hence a <= b by A1, A2, YELLOW_3:3; :: thesis: verum

( not b

set f = sup_op L;

assume x <= y ; :: thesis: for b

( not b

then A1: ( x `1 <= y `1 & x `2 <= y `2 ) by YELLOW_3:12;

A2: ( (sup_op L) . x = (x `1) "\/" (x `2) & (sup_op L) . y = (y `1) "\/" (y `2) ) by Th34;

let a, b be Element of L; :: thesis: ( not a = (sup_op L) . x or not b = (sup_op L) . y or a <= b )

assume ( a = (sup_op L) . x & b = (sup_op L) . y ) ; :: thesis: a <= b

hence a <= b by A1, A2, YELLOW_3:3; :: thesis: verum