set t = { (tau1 . p) where p is Element of LTLB_WFF : p in X } ;
union { (tau1 . p) where p is Element of LTLB_WFF : p in X } c= LTLB_WFF

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union { (tau1 . p) where p is Element of LTLB_WFF : p in X } or x in LTLB_WFF )
assume x in union { (tau1 . p) where p is Element of LTLB_WFF : p in X } ; :: thesis: x in LTLB_WFF
then consider y being set such that
A1: x in y and
A2: y in { (tau1 . p) where p is Element of LTLB_WFF : p in X } by TARSKI:def 4;
ex p being Element of LTLB_WFF st
( y = tau1 . p & p in X ) by A2;
hence x in LTLB_WFF by A1; :: thesis: verum

end;

then reconsider ut = union { (tau1 . p) where p is Element of LTLB_WFF : p in X } as Subset of LTLB_WFF ;
for x being set holds
( x in ut iff ex A being Element of LTLB_WFF st
( A in X & x in tau1 . A ) )

proof

let x be set ; :: thesis: ( x in ut iff ex A being Element of LTLB_WFF st
( A in X & x in tau1 . A ) )

hereby :: thesis: ( ex A being Element of LTLB_WFF st
( A in X & x in tau1 . A ) implies x in ut )

assume x in ut ; :: thesis: ex A being Element of LTLB_WFF st
( A in X & x in tau1 . A )
then consider y being set such that
A3: x in y and
A4: y in { (tau1 . p) where p is Element of LTLB_WFF : p in X } by TARSKI:def 4;
ex p being Element of LTLB_WFF st
( y = tau1 . p & p in X ) by A4;
hence ex A being Element of LTLB_WFF st
( A in X & x in tau1 . A ) by A3; :: thesis: verum

end;

given A being Element of LTLB_WFF such that A5: A in X and
A6: x in tau1 . A ; :: thesis: x in ut
tau1 . A in { (tau1 . p) where p is Element of LTLB_WFF : p in X } by A5;
hence x in ut by TARSKI:def 4, A6; :: thesis: verum

end;

hence ex b₁ being Subset of LTLB_WFF st
for x being set holds
( x in b₁ iff ex A being Element of LTLB_WFF st
( A in X & x in tau1 . A ) ) ; :: thesis: verum