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

end;

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