( 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 Def5, Lm2;
hence ConstantNet (R,p) is transitive by Lm2; :: thesis: verum