let L be non empty OrthoLattStr ; :: thesis: ( L is de_Morgan & L is involutive implies L is DeMorgan )
assume A1: ( L is de_Morgan & L is involutive ) ; :: thesis: L is DeMorgan
let x, y be Element of L; :: according to NELSON_1:def 1 :: thesis: (x "/\" y) ` = (x `) "\/" (y `)
x "/\" y = ((x `) "\/" (y `)) ` by A1;
hence (x "/\" y) ` = (x `) "\/" (y `) by A1; :: thesis: verum