for P being non empty complete Poset
for V being non empty Subset of P holds uparrow (sup V) = meet { (uparrow u) where u is Element of P : u in V }