:: deftheorem defines VarPoset ABCMIZ_1:def 51 :
VarPoset = (InclPoset { (varcl A) where A is finite Subset of Vars : verum } ) opp ;