theorem Th15: :: YELLOW19:15

for T being non empty 1-sorted
for F being Filter of (BoolePoset ([#] T))
for A being non empty Subset of T holds
( A in F iff a_net F is_eventually_in A )