theorem :: CARDFIL2:61

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