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 & (~ x) ~ = ~ x & ~ y = y & (~ y) ~ = ~ y ) ;
hence ( x <= y iff ~ x >= ~ y ) by LATTICE3:9; :: thesis: verum