deffunc H₁( Element of LTLB_WFF ) -> Element of LTLB_WFF = 'G' F;
A1: F is finite ;
{ H₁(w) where w is Element of LTLB_WFF : w in F } is finite from FRAENKEL:sch 21(A1);
hence 'G' F is finite ; :: thesis: verum