let K, L be non empty OrthoLattStr ; :: thesis: ( OrthoLattStr(# the carrier of K, the L_join of K, the L_meet of K, the Compl of K #) = OrthoLattStr(# the carrier of L, the L_join of L, the L_meet of L, the Compl of L #) & K is de_Morgan implies L is de_Morgan )
assume that
A1: OrthoLattStr(# the carrier of K, the L_join of K, the L_meet of K, the Compl of K #) = OrthoLattStr(# the carrier of L, the L_join of L, the L_meet of L, the Compl of L #) and
A2: K is de_Morgan ; :: thesis: L is de_Morgan
for x, y being Element of L holds x "/\" y = ((x `) "\/" (y `)) `

proof

let x, y be Element of L; :: thesis: x "/\" y = ((x `) "\/" (y `)) `
reconsider x9 = x, y9 = y as Element of K by A1;
A3: ( x ` = x9 ` & y ` = y9 ` ) by A1, Th18;
x "/\" y = x9 "/\" y9 by A1
.= ((x9 `) "\/" (y9 `)) ` by A2, ROBBINS1:def 23
.= ((x `) "\/" (y `)) ` by A1, A3, Th18 ;
hence x "/\" y = ((x `) "\/" (y `)) ` ; :: thesis: verum

end;

hence L is de_Morgan by ROBBINS1:def 23; :: thesis: verum