set IR = the Relation of the carrier of R;
set L = LattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R #);
take
LattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R #)
; LattStr(# the carrier of LattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R #), the L_join of LattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R #), the L_meet of LattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R #) #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #)
thus
LattStr(# the carrier of LattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R #), the L_join of LattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R #), the L_meet of LattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R #) #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #)
; verum