theorem Th43: :: CARDFIL2:93

for L being non empty 1-sorted
for B being set
for s being sequence of the carrier of L holds
( sequence_to_net s is_eventually_in B iff ex i being Element of (sequence_to_net s) st
for j being Element of (sequence_to_net s) st i <= j holds
(sequence_to_net s) . j in B ) ;