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

{ (Sub . A) where A is Element of LTLB_WFF : A in X } c= bool LTLB_WFF

{ (Sub . A) where A is Element of LTLB_WFF : A in X } c= bool LTLB_WFF

proof

hence
{ (Sub . A) where A is Element of LTLB_WFF : A in X } is Subset of (bool LTLB_WFF)
; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (Sub . A) where A is Element of LTLB_WFF : A in X } or x in bool LTLB_WFF )

assume x in { (Sub . A) where A is Element of LTLB_WFF : A in X } ; :: thesis: x in bool LTLB_WFF

then ex A being Element of LTLB_WFF st

( x = Sub . A & A in X ) ;

hence x in bool LTLB_WFF ; :: thesis: verum

end;assume x in { (Sub . A) where A is Element of LTLB_WFF : A in X } ; :: thesis: x in bool LTLB_WFF

then ex A being Element of LTLB_WFF st

( x = Sub . A & A in X ) ;

hence x in bool LTLB_WFF ; :: thesis: verum