let L be with_suprema 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:22;
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:22;
hence (x "\/" y) ~ >= d by LATTICE3:9; :: thesis: verum

end;

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