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