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 A2: 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 ` )) `
((x ` ) "\/" (y ` )) ` [= (y ` ) ` by A2, LATTICES:22;
then A3: ((x ` ) "\/" (y ` )) ` [= y by ROBBINS3:def 6;
( x ` [= (x "/\" y) ` & y ` [= (x "/\" y) ` ) by A2, LATTICES:23;
then (x ` ) "\/" (y ` ) [= (x "/\" y) ` by FILTER_0:6;
then ((x "/\" y) ` ) ` [= ((x ` ) "\/" (y ` )) ` by A2;
then A4: x "/\" y [= ((x ` ) "\/" (y ` )) ` by ROBBINS3:def 6;
((x ` ) "\/" (y ` )) ` [= (x ` ) ` by A2, LATTICES:22;
then ((x ` ) "\/" (y ` )) ` [= x by ROBBINS3:def 6;
then ((x ` ) "\/" (y ` )) ` [= x "/\" y by A3, FILTER_0:7;
hence x "/\" y = ((x ` ) "\/" (y ` )) ` by A4, LATTICES:26; :: thesis: verum