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

for x being set holds

( x in ut iff ex A being Element of LTLB_WFF st

( A in X & x in tau1 . A ) )_{1} being Subset of LTLB_WFF st

for x being set holds

( x in b_{1} iff ex A being Element of LTLB_WFF st

( A in X & x in tau1 . A ) ) ; :: thesis: verum

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

proof

then reconsider ut = union { (tau1 . p) where p is Element of LTLB_WFF : p in X } as Subset of LTLB_WFF ;
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;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

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

hence
ex b
let x be set ; :: thesis: ( x in ut iff ex A being Element of LTLB_WFF st

( A in X & x in tau1 . A ) )

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

given A being Element of LTLB_WFF such that A5:
A in X
and ( 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;( 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

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

for x being set holds

( x in b

( A in X & x in tau1 . A ) ) ; :: thesis: verum