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 ;
hence (x `) ` = x ; :: thesis: verum
end;
hence L is involutive ; :: thesis: verum