let L be with_infima Poset; :: thesis: for x, y being Element of (L opp ) holds (~ x) "/\" (~ y) = x "\/" y
let x, y be Element of (L opp ); :: thesis: (~ x) "/\" (~ y) = x "\/" y
( ~ x = x & (~ x) ~ = ~ x & ~ y = y & (~ y) ~ = ~ y ) ;
hence (~ x) "/\" (~ y) = x "\/" y by Th21; :: thesis: verum