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₁ = (inf_op L) . x or not b₂ = (inf_op L) . y or b₁ <= b₂ ) )
set f = inf_op L;
assume x <= y ; :: thesis: for b₁, b₂ being Element of the carrier of L holds
( not b₁ = (inf_op L) . x or not b₂ = (inf_op L) . y or b₁ <= 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