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 #) ; :: thesis: 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 #) ; :: thesis: verum