consider IR being Relation of the carrier of R;
set L = OrthoLattRelStr(# the carrier of R,the L_join of R,the L_meet of R,IR,the Compl of R #);
take OrthoLattRelStr(# the carrier of R,the L_join of R,the L_meet of R,IR,the Compl of R #) ; :: thesis: OrthoLattStr(# the carrier of OrthoLattRelStr(# the carrier of R,the L_join of R,the L_meet of R,IR,the Compl of R #),the L_join of OrthoLattRelStr(# the carrier of R,the L_join of R,the L_meet of R,IR,the Compl of R #),the L_meet of OrthoLattRelStr(# the carrier of R,the L_join of R,the L_meet of R,IR,the Compl of R #),the Compl of OrthoLattRelStr(# the carrier of R,the L_join of R,the L_meet of R,IR,the Compl of R #) #) = OrthoLattStr(# the carrier of R,the L_join of R,the L_meet of R,the Compl of R #)
thus OrthoLattStr(# the carrier of OrthoLattRelStr(# the carrier of R,the L_join of R,the L_meet of R,IR,the Compl of R #),the L_join of OrthoLattRelStr(# the carrier of R,the L_join of R,the L_meet of R,IR,the Compl of R #),the L_meet of OrthoLattRelStr(# the carrier of R,the L_join of R,the L_meet of R,IR,the Compl of R #),the Compl of OrthoLattRelStr(# the carrier of R,the L_join of R,the L_meet of R,IR,the Compl of R #) #) = OrthoLattStr(# the carrier of R,the L_join of R,the L_meet of R,the Compl of R #) ; :: thesis: verum