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