scheme :: WAYBEL_0:sch 1
HoldsEventually{ F₁() -> non empty RelStr , F₂() -> non empty NetStr over F₁(), P₁[ set ] } :

( F₂() is_eventually_in { (F₂() . k) where k is Element of F₂() : P₁[F₂() . k] } iff ex i being Element of F₂() st
for j being Element of F₂() st i <= j holds
P₁[F₂() . j] )