let L be RelStr ; :: thesis: for x, y being Element of (L opp) holds
( x <= y iff ~ x >= ~ y )
let x, y be Element of (L opp); :: thesis: ( x <= y iff ~ x >= ~ y )
( (~ x) ~ = ~ x & (~ y) ~ = ~ y ) ;
hence ( x <= y iff ~ x >= ~ y ) by LATTICE3:9; :: thesis: verum