( RelStr(# the carrier of (ConstantNet R,p),the InternalRel of (ConstantNet R,p) #) = RelStr(# the carrier of R,the InternalRel of R #) & RelStr(# the carrier of R,the InternalRel of R #) is transitive ) by Def7, Lm2;
hence ConstantNet R,p is transitive by Lm2; :: thesis: verum