for x being set holds
( x is Element of VarPoset iff ( x is finite Subset of Vars & varcl x = x ) )