:: deftheorem defines BOOL2F CARDFIL2:def 20 :
for T being non empty TopSpace
for F being proper Filter of (BoolePoset ([#] T)) holds BOOL2F F = F;