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