for S being non empty reflexive RelStr
for D being non empty Subset of S holds
( the mapping of (Net-Str D) = id D & the carrier of (Net-Str D) = D & Net-Str D is full SubRelStr of S )