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