let T be non empty 1-sorted ; :: thesis: for N being non empty NetStr over T

for A being set holds

( A in a_filter N iff ( N is_eventually_in A & A is Subset of T ) )

let N be non empty NetStr over T; :: thesis: for A being set holds

( A in a_filter N iff ( N is_eventually_in A & A is Subset of T ) )

let B be set ; :: thesis: ( B in a_filter N iff ( N is_eventually_in B & B is Subset of T ) )

( B in a_filter N iff ex A being Subset of T st

( B = A & N is_eventually_in A ) ) ;

hence ( B in a_filter N iff ( N is_eventually_in B & B is Subset of T ) ) ; :: thesis: verum

for A being set holds

( A in a_filter N iff ( N is_eventually_in A & A is Subset of T ) )

let N be non empty NetStr over T; :: thesis: for A being set holds

( A in a_filter N iff ( N is_eventually_in A & A is Subset of T ) )

let B be set ; :: thesis: ( B in a_filter N iff ( N is_eventually_in B & B is Subset of T ) )

( B in a_filter N iff ex A being Subset of T st

( B = A & N is_eventually_in A ) ) ;

hence ( B in a_filter N iff ( N is_eventually_in B & B is Subset of T ) ) ; :: thesis: verum