consider IR being Relation of the carrier of R;
set L = LattRelStr(# the carrier of R,the L_join of R,the L_meet of R,IR #);
take LattRelStr(# the carrier of R,the L_join of R,the L_meet of R,IR #) ; :: thesis: LattStr(# the carrier of LattRelStr(# the carrier of R,the L_join of R,the L_meet of R,IR #),the L_join of LattRelStr(# the carrier of R,the L_join of R,the L_meet of R,IR #),the L_meet of LattRelStr(# the carrier of R,the L_join of R,the L_meet of R,IR #) #) = 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,IR #),the L_join of LattRelStr(# the carrier of R,the L_join of R,the L_meet of R,IR #),the L_meet of LattRelStr(# the carrier of R,the L_join of R,the L_meet of R,IR #) #) = LattStr(# the carrier of R,the L_join of R,the L_meet of R #) ; :: thesis: verum