theorem :: WAYBEL_0:8

for L being non empty 1-sorted
for N being non empty NetStr over L
for X, Y being set st X c= Y holds
( ( N is_eventually_in X implies N is_eventually_in Y ) & ( N is_often_in X implies N is_often_in Y ) )