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

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in union { (tau1 . p) where p is Element of LTLB_WFF : p in X } ; :: thesis:
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:

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 ) )

let x be set ; :: thesis:

assume x in ut ; :: thesis:
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:

end;

given A being Element of LTLB_WFF such that A5: A in X and
A6: x in tau1 . A ; :: thesis:
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:

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: