theorem Th14: :: YELLOW19:14

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