set IR = the Relation of the carrier of R;
set L = OrthoLattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R, the Compl of R #);
take
OrthoLattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R, the Compl of R #)
; OrthoLattStr(# the carrier of OrthoLattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R, the Compl of R #), the L_join of OrthoLattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R, the Compl of R #), the L_meet of OrthoLattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R, the Compl of R #), the Compl of OrthoLattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R, 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, the Relation of the carrier of R, the Compl of R #), the L_join of OrthoLattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R, the Compl of R #), the L_meet of OrthoLattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R, the Compl of R #), the Compl of OrthoLattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R, the Compl of R #) #) = OrthoLattStr(# the carrier of R, the L_join of R, the L_meet of R, the Compl of R #)
; verum