let X be Subset of LTLB_WFF; :: thesis: tau X = union { (tau1 . p) where p is Element of LTLB_WFF : p in X }

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

assume x in union { (tau1 . p) where p is Element of LTLB_WFF : p in X } ; :: thesis: x in tau X

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;

A5: ex p being Element of LTLB_WFF st

( y = tau1 . p & p in X ) by A4;

then reconsider x1 = x as Element of LTLB_WFF by A3;

thus x in tau X by A5, A3, Def5; :: thesis: verum

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

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: union { (tau1 . p) where p is Element of LTLB_WFF : p in X } c= tau X

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 tau X )let x be object ; :: thesis: ( x in tau X implies x in union { (tau1 . p) where p is Element of LTLB_WFF : p in X } )

assume x in tau X ; :: thesis: x in union { (tau1 . p) where p is Element of LTLB_WFF : p in X }

then consider p being Element of LTLB_WFF such that

A1: p in X and

A2: x in tau1 . p by Def5;

tau1 . p in { (tau1 . p) where p is Element of LTLB_WFF : p in X } by A1;

hence x in union { (tau1 . p) where p is Element of LTLB_WFF : p in X } by TARSKI:def 4, A2; :: thesis: verum

end;assume x in tau X ; :: thesis: x in union { (tau1 . p) where p is Element of LTLB_WFF : p in X }

then consider p being Element of LTLB_WFF such that

A1: p in X and

A2: x in tau1 . p by Def5;

tau1 . p in { (tau1 . p) where p is Element of LTLB_WFF : p in X } by A1;

hence x in union { (tau1 . p) where p is Element of LTLB_WFF : p in X } by TARSKI:def 4, A2; :: thesis: verum

assume x in union { (tau1 . p) where p is Element of LTLB_WFF : p in X } ; :: thesis: x in tau X

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;

A5: ex p being Element of LTLB_WFF st

( y = tau1 . p & p in X ) by A4;

then reconsider x1 = x as Element of LTLB_WFF by A3;

thus x in tau X by A5, A3, Def5; :: thesis: verum