theorem Th27: :: WAYBEL11:27

for S being non empty 1-sorted
for e being Element of S
for X being set holds
( Net-Str e is_eventually_in X iff e in X )