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 involutive implies L is involutive )
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 involutive ; :: thesis: L is involutive
for x being Element of L holds (x ` ) ` = x

proof

let x be Element of L; :: thesis: (x ` ) ` = x
reconsider x9 = x as Element of K by A1;
x ` = x9 ` by A1, Th18;
then (x ` ) ` = (x9 ` ) ` by A1, Th18
.= x by A2, Def6 ;
hence (x ` ) ` = x ; :: thesis: verum

end;

hence L is involutive by Def6; :: thesis: verum