deffunc H₃( Element of LTLB_WFF ) -> Element of bool LTLB_WFF = Sub . X;
A1: X is finite ;
{ H₃(A) where A is Element of LTLB_WFF : A in X } is finite from FRAENKEL:sch 21(A1);
hence Subt X is finite ; :: thesis: Subt X is finite-membered
let x be set ; :: according to FINSET_1:def 6 :: thesis: ( not x in Subt X or x is finite )
assume x in Subt X ; :: thesis: x is finite
then ex A being Element of LTLB_WFF st
( x = Sub . A & A in X ) ;
hence x is finite ; :: thesis: verum