for T being non empty TopSpace
for F being Filter of the carrier of T ex F1 being proper Filter of (BoolePoset the carrier of T) st F = F1