RelStr(# the carrier of (R --> p),the InternalRel of (R --> p) #) = RelStr(# the carrier of R,the InternalRel of R #) by Def7;
hence not the carrier of (R --> p) is empty ; :: according to STRUCT_0:def 1 :: thesis: verum