A1: RelStr(# the carrier of (R --> p),the InternalRel of (R --> p) #) = RelStr(# the carrier of R,the InternalRel of R #) by Def7;
RelStr(# the carrier of R,the InternalRel of R #) is directed by Lm1;
hence R --> p is directed by A1, Lm1; :: thesis: verum