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