A1: now

let L be RelStr ; :: thesis: for x being Element of L
for X being set st x is_<=_than X holds
x ~ is_>=_than X
let x be Element of L; :: thesis: for X being set st x is_<=_than X holds
x ~ is_>=_than X
let X be set ; :: thesis: ( x is_<=_than X implies x ~ is_>=_than X )
assume A2: x is_<=_than X ; :: thesis: x ~ is_>=_than X
thus x ~ is_>=_than X :: thesis: verum

proof

let a be Element of (L opp ); :: according to LATTICE3:def 9 :: thesis: ( not a in X or a <= x ~ )
assume A3: a in X ; :: thesis: a <= x ~
A4: ( (~ a) ~ = ~ a & ~ a = a ) ;
x <= ~ a by A2, A3, LATTICE3:def 8;
hence a <= x ~ by A4, LATTICE3:9; :: thesis: verum

end;

end;

A5: now

let L be RelStr ; :: thesis: for x being Element of L
for X being set st x is_>=_than X holds
x ~ is_<=_than X
let x be Element of L; :: thesis: for X being set st x is_>=_than X holds
x ~ is_<=_than X
let X be set ; :: thesis: ( x is_>=_than X implies x ~ is_<=_than X )
assume A6: x is_>=_than X ; :: thesis: x ~ is_<=_than X
thus x ~ is_<=_than X :: thesis: verum

proof

let a be Element of (L opp ); :: according to LATTICE3:def 8 :: thesis: ( not a in X or x ~ <= a )
assume A7: a in X ; :: thesis: x ~ <= a
A8: ( (~ a) ~ = ~ a & ~ a = a ) ;
x >= ~ a by A6, A7, LATTICE3:def 9;
hence x ~ <= a by A8, LATTICE3:9; :: thesis: verum

end;

end;

let L be RelStr ; :: thesis: for x being Element of L
for X being set holds
( ( x is_<=_than X implies x ~ is_>=_than X ) & ( x ~ is_>=_than X implies x is_<=_than X ) & ( x is_>=_than X implies x ~ is_<=_than X ) & ( x ~ is_<=_than X implies x is_>=_than X ) )
let x be Element of L; :: thesis: for X being set holds
( ( x is_<=_than X implies x ~ is_>=_than X ) & ( x ~ is_>=_than X implies x is_<=_than X ) & ( x is_>=_than X implies x ~ is_<=_than X ) & ( x ~ is_<=_than X implies x is_>=_than X ) )
let X be set ; :: thesis: ( ( x is_<=_than X implies x ~ is_>=_than X ) & ( x ~ is_>=_than X implies x is_<=_than X ) & ( x is_>=_than X implies x ~ is_<=_than X ) & ( x ~ is_<=_than X implies x is_>=_than X ) )
( (x ~ ) ~ is_<=_than X implies x is_<=_than X ) by YELLOW_0:2;
hence ( x is_<=_than X iff x ~ is_>=_than X ) by A1, A5; :: thesis: ( x is_>=_than X iff x ~ is_<=_than X )
( (x ~ ) ~ is_>=_than X implies x is_>=_than X ) by YELLOW_0:2;
hence ( x is_>=_than X iff x ~ is_<=_than X ) by A1, A5; :: thesis: verum