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 ) )

A1: now :: thesis: for L being RelStr
for x being Element of L
for X being set st x is_<=_than X holds
x ~ is_>=_than X

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 a in X ; :: thesis: a <= x ~
then ( (~ a) ~ = ~ a & x <= ~ a ) by A2;
hence a <= x ~ by LATTICE3:9; :: thesis: verum

end;

end;

A3: now :: thesis: for L being RelStr
for x being Element of L
for X being set st x is_>=_than X holds
x ~ is_<=_than X

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 A4: 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 a in X ; :: thesis: x ~ <= a
then ( (~ a) ~ = ~ a & x >= ~ a ) by A4;
hence x ~ <= a by LATTICE3:9; :: thesis: verum

end;

end;

( (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, A3; :: 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, A3; :: thesis: verum