theorem :: WAYBEL_0:10

for L being non empty 1-sorted
for N being non empty NetStr over L
for X being set holds
( N is_often_in X iff not N is_eventually_in the carrier of L \ X )