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 <= x & x "/\" y <= y ) by YELLOW_0:23;
then A1: ( (x "/\" y) ~ >= x ~ & (x "/\" y) ~ >= y ~ ) by LATTICE3:9;
A2: ( x ~ = x & ~ (x ~ ) = x ~ & y ~ = y & ~ (y ~ ) = y ~ ) ;

now

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 ( ~ d <= x "/\" y & (~ d) ~ = ~ d & ~ d = d ) by YELLOW_0:23;
hence (x "/\" y) ~ <= d by LATTICE3:9; :: thesis: verum

end;

hence x "/\" y = (x ~ ) "\/" (y ~ ) by A1, YELLOW_0:22; :: thesis: verum