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 } ;
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 ; :: 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;
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 )
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