for T being non empty RelStr
for N being net of T
for X being set st N is_eventually_in X holds
ex i being Element of N st
( N . i in X & rng the mapping of (N | i) c= X )