theorem Th112: :: ABCMIZ_1:112

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