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