theorem Th13: :: YELLOW19:13

for T being non empty 1-sorted
for F being Filter of (BoolePoset ([#] T)) holds F \ {{}} = a_filter (a_net F)