let L be non empty OrthoLattStr ; :: thesis: ( L is DeMorgan & L is involutive implies L is de_Morgan )
assume A1: ( L is DeMorgan & L is involutive ) ; :: thesis: L is de_Morgan

now :: thesis: for x, y being Element of L holds ((x `) "\/" (y `)) ` = x "/\" y

let x, y be Element of L; :: thesis: ((x `) "\/" (y `)) ` = x "/\" y
(x `) "\/" (y `) = (x "/\" y) ` by A1;
hence ((x `) "\/" (y `)) ` = x "/\" y by A1; :: thesis: verum

end;

hence L is de_Morgan ; :: thesis: verum