consider A0 being finite Subset of Vars ;
set V = { (varcl A) where A is finite Subset of Vars : verum } ;
varcl A0 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