set c = { (untn (A,B)) where A, B is Element of LTLB_WFF : A 'U' B in X } ;
{ (untn (A,B)) where A, B is Element of LTLB_WFF : A 'U' B in X } c= LTLB_WFF

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (untn (A,B)) where A, B is Element of LTLB_WFF : A 'U' B in X } or x in LTLB_WFF )
assume x in { (untn (A,B)) where A, B is Element of LTLB_WFF : A 'U' B in X } ; :: thesis: x in LTLB_WFF
then ex A, B being Element of LTLB_WFF st
( x = untn (A,B) & A 'U' B in X ) ;
hence x in LTLB_WFF ; :: thesis: verum

end;

hence { (untn (A,B)) where A, B is Element of LTLB_WFF : A 'U' B in X } is Subset of LTLB_WFF ; :: thesis: verum