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