set a = { (comp P) where P is Element of [:(LTLB_WFF **),(LTLB_WFF **):] : P in X } ;
{ (comp P) where P is Element of [:(LTLB_WFF **),(LTLB_WFF **):] : P in X } c= bool [:(LTLB_WFF **),(LTLB_WFF **):]

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (comp P) where P is Element of [:(LTLB_WFF **),(LTLB_WFF **):] : P in X } or x in bool [:(LTLB_WFF **),(LTLB_WFF **):] )
assume x in { (comp P) where P is Element of [:(LTLB_WFF **),(LTLB_WFF **):] : P in X } ; :: thesis: x in bool [:(LTLB_WFF **),(LTLB_WFF **):]
then ex P being PNPair st
( x = comp P & P in X ) ;
hence x in bool [:(LTLB_WFF **),(LTLB_WFF **):] ; :: thesis: verum

end;

then reconsider a1 = { (comp P) where P is Element of [:(LTLB_WFF **),(LTLB_WFF **):] : P in X } as Subset-Family of [:(LTLB_WFF **),(LTLB_WFF **):] ;
union a1 is Subset of [:(LTLB_WFF **),(LTLB_WFF **):] ;
hence union { (comp P) where P is Element of [:(LTLB_WFF **),(LTLB_WFF **):] : P in X } is Subset of [:(LTLB_WFF **),(LTLB_WFF **):] ; :: thesis: verum