let L be non empty Lattice-like involutive OrthoLattStr ; :: thesis: ( L is de_Morgan iff for a, b being Element of L st a [= b holds
b ` [= a ` )
thus ( L is de_Morgan implies for a, b being Element of L st a [= b holds
b ` [= a ` ) :: thesis: ( ( for a, b being Element of L st a [= b holds
b ` [= a ` ) implies L is de_Morgan )

proof

assume a1: L is de_Morgan ; :: thesis: for a, b being Element of L st a [= b holds
b ` [= a `
let a, b be Element of L; :: thesis: ( a [= b implies b ` [= a ` )
assume a [= b ; :: thesis: b ` [= a `
then a ` = (a "/\" b) ` by LATTICES:21
.= (((a ` ) "\/" (b ` )) ` ) ` by a1, ROBBINS1:def 23
.= (b ` ) "\/" (a ` ) by ROBBINS3:def 6 ;
then (a ` ) "/\" (b ` ) = b ` by LATTICES:def 9;
hence b ` [= a ` by LATTICES:21; :: thesis: verum

end;

assume a: for a, b being Element of L st a [= b holds
b ` [= a ` ; :: thesis: L is de_Morgan
let x, y be Element of L; :: according to ROBBINS1:def 23 :: thesis: x "/\" y = ((x ` ) "\/" (y ` )) `
b: x ` [= (x "/\" y) ` by a, LATTICES:23;
c: y ` [= (x "/\" y) ` by a, LATTICES:23;
(x ` ) "\/" (y ` ) [= (x "/\" y) ` by b, c, FILTER_0:6;
then ((x "/\" y) ` ) ` [= ((x ` ) "\/" (y ` )) ` by a;
then A: x "/\" y [= ((x ` ) "\/" (y ` )) ` by ROBBINS3:def 6;
((x ` ) "\/" (y ` )) ` [= (x ` ) ` by a, LATTICES:22;
then d: ((x ` ) "\/" (y ` )) ` [= x by ROBBINS3:def 6;
((x ` ) "\/" (y ` )) ` [= (y ` ) ` by a, LATTICES:22;
then e: ((x ` ) "\/" (y ` )) ` [= y by ROBBINS3:def 6;
((x ` ) "\/" (y ` )) ` [= x "/\" y by d, e, FILTER_0:7;
hence x "/\" y = ((x ` ) "\/" (y ` )) ` by A, LATTICES:26; :: thesis: verum