theorem :: WAYBEL15:2

for X being set
for a being Element of (BoolePoset X) holds uparrow a = { Y where Y is Subset of X : a c= Y }