for X being non empty set
for B being filter_base of X
for L being Subset of (BoolePoset X) st L = B holds
<.B.) = uparrow L by Th04;