set A = the BinOp of the carrier of R;
set L = LattRelStr(# the carrier of R, the BinOp of the carrier of R, the BinOp of the carrier of R, the InternalRel of R #);
take
LattRelStr(# the carrier of R, the BinOp of the carrier of R, the BinOp of the carrier of R, the InternalRel of R #)
; RelStr(# the carrier of LattRelStr(# the carrier of R, the BinOp of the carrier of R, the BinOp of the carrier of R, the InternalRel of R #), the InternalRel of LattRelStr(# the carrier of R, the BinOp of the carrier of R, the BinOp of the carrier of R, the InternalRel of R #) #) = RelStr(# the carrier of R, the InternalRel of R #)
thus
RelStr(# the carrier of LattRelStr(# the carrier of R, the BinOp of the carrier of R, the BinOp of the carrier of R, the InternalRel of R #), the InternalRel of LattRelStr(# the carrier of R, the BinOp of the carrier of R, the BinOp of the carrier of R, the InternalRel of R #) #) = RelStr(# the carrier of R, the InternalRel of R #)
; verum