theorem Th4: :: ROBBINS4:4

for L being non empty Lattice-like involutive OrthoLattStr holds
( L is de_Morgan iff for a, b being Element of L st a [= b holds
b ` [= a ` )