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 `)) ` hence L is de_Morgan by ROBBINS1:def 23; :: thesis: verum