set t = { () where p is Element of LTLB_WFF : p in X } ;
union { () 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 { () where p is Element of LTLB_WFF : p in X } or x in LTLB_WFF )
assume x in union { () 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 { () 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 { () 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 { () 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 { () where p is Element of LTLB_WFF : p in X } by A5;
hence x in ut by ; :: thesis: verum
end;
hence ex b1 being Subset of LTLB_WFF st
for x being set holds
( x in b1 iff ex A being Element of LTLB_WFF st
( A in X & x in tau1 . A ) ) ; :: thesis: verum