set A0 = the finite Subset of Vars;
set V = { (varcl A) where A is finite Subset of Vars : verum } ;
varcl the finite Subset of Vars in { (varcl A) where A is finite Subset of Vars : verum } ;
then reconsider V = { (varcl A) where A is finite Subset of Vars : verum } as non empty set ;
reconsider P = InclPoset V as non empty Poset ;
not P opp is empty ;
hence (InclPoset { (varcl A) where A is finite Subset of Vars : verum } ) opp is non empty strict Poset ; :: thesis: verum