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