for X being non empty Subset of VarPoset holds
( ex_sup_of X, VarPoset & sup X = meet X )