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