set A = { (tau1 . p) where p is Element of LTLB_WFF : p in X } ;
deffunc H₃( Element of LTLB_WFF ) -> Element of bool LTLB_WFF = tau1 . X;
A1: for x being set st x in { (tau1 . p) where p is Element of LTLB_WFF : p in X } holds
x is finite

proof

let x be set ; :: thesis: ( x in { (tau1 . p) where p is Element of LTLB_WFF : p in X } implies x is finite )
assume x in { (tau1 . p) where p is Element of LTLB_WFF : p in X } ; :: thesis: x is finite
then ex p being Element of LTLB_WFF st
( x = tau1 . p & p in X ) ;
hence x is finite ; :: thesis: verum

end;

set B = { H₃(p) where p is Element of LTLB_WFF : p in X } ;
A2: X is finite ;
A3: { H₃(p) where p is Element of LTLB_WFF : p in X } is finite from FRAENKEL:sch 21(A2);
tau X = union { (tau1 . p) where p is Element of LTLB_WFF : p in X } by Th15;
hence tau X is finite by A3, FINSET_1:7, A1; :: thesis: verum