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