let R be RelStr ; :: thesis: for T being non empty 1-sorted
for p being Element of T holds the carrier of (ConstantNet (R,p)) = the carrier of R
let T be non empty 1-sorted ; :: thesis: for p being Element of T holds the carrier of (ConstantNet (R,p)) = the carrier of R
let p be Element of T; :: thesis: the carrier of (ConstantNet (R,p)) = the carrier of R
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 the carrier of (ConstantNet (R,p)) = the carrier of R ; :: thesis: verum