set V = { (varcl A) where A is finite Subset of Vars : verum } ;
{} Vars in { (varcl A) where A is finite Subset of Vars : verum } by Th11;
then ( VarPoset opp is lower-bounded & (Bottom (InclPoset { (varcl A) where A is finite Subset of Vars : verum } )) ~ = {} & VarPoset opp = InclPoset { (varcl A) where A is finite Subset of Vars : verum } ) by YELLOW_1:13, YELLOW_7:31;
hence Top VarPoset = {} by YELLOW_7:33; :: thesis: verum