let L be with_infima Poset; :: thesis: for x, y being Element of L holds x "/\" y = (x ~) "\/" (y ~)
let x, y be Element of L; :: thesis: x "/\" y = (x ~) "\/" (y ~)
x "/\" y <= y by YELLOW_0:23;
then A1: (x "/\" y) ~ >= y ~ by LATTICE3:9;
A2: ( ~ (x ~) = x ~ & ~ (y ~) = y ~ ) ;

A3: now :: thesis: for d being Element of (L opp) st d >= x ~ & d >= y ~ holds
(x "/\" y) ~ <= d

let d be Element of (L opp); :: thesis: ( d >= x ~ & d >= y ~ implies (x "/\" y) ~ <= d )
assume ( d >= x ~ & d >= y ~ ) ; :: thesis: (x "/\" y) ~ <= d
then ( ~ d <= x & ~ d <= y ) by A2, Th1;
then A4: ~ d <= x "/\" y by YELLOW_0:23;
(~ d) ~ = ~ d ;
hence (x "/\" y) ~ <= d by A4, LATTICE3:9; :: thesis: verum

end;

x "/\" y <= x by YELLOW_0:23;
then (x "/\" y) ~ >= x ~ by LATTICE3:9;
hence x "/\" y = (x ~) "\/" (y ~) by A1, A3, YELLOW_0:22; :: thesis: verum