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 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 #) & 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 x' = x as Element of K by A1;
x ` = x' ` by A1, Th18;
then (x ` ) ` = (x' ` ) ` by A1, Th18
.= x by A1, Def6 ;
hence (x ` ) ` = x ; :: thesis: verum

end;

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