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} = (inf_op L) . x or not b_{2} = (inf_op L) . y or b_{1} <= b_{2} ) )

set f = inf_op L;

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

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

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

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

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

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

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

( not b

set f = inf_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: ( (inf_op L) . x = (x `1) "/\" (x `2) & (inf_op L) . y = (y `1) "/\" (y `2) ) by Th31;

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

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

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