set b = { (P ^) where P is Element of [:(LTLB_WFF **),(LTLB_WFF **):] : P in F } ;
{ (P ^) where P is Element of [:(LTLB_WFF **),(LTLB_WFF **):] : P in F } c= LTLB_WFF

proof

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

end;

hence { (P ^) where P is Element of [:(LTLB_WFF **),(LTLB_WFF **):] : P in F } is Subset of LTLB_WFF ; :: thesis: verum