let x, y be Element of [:L,L:]; :: according to ORDERS_3:def 5 :: thesis: ( not x <= y or for b₁, b₂ being Element of the carrier of L holds
( not b₁ = (sup_op L) . x or not b₂ = (sup_op L) . y or b₁ <= b₂ ) )
set f = sup_op L;
assume x <= y ; :: thesis: for b₁, b₂ being Element of the carrier of L holds
( not b₁ = (sup_op L) . x or not b₂ = (sup_op L) . y or b₁ <= 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