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