:: deftheorem Def5 defines ConstantNet YELLOW_6:def 5 :
for R being RelStr
for T being non empty 1-sorted
for p being Element of T
for b₄ being strict NetStr over T holds
( b₄ = ConstantNet (R,p) iff ( RelStr(# the carrier of b₄, the InternalRel of b₄ #) = RelStr(# the carrier of R, the InternalRel of R #) & the mapping of b₄ = the carrier of b₄ --> p ) );