:: deftheorem defines 'X' MODELC_2:def 65 :
for W being Subset of LTL_WFF holds 'X' W = { x where x is LTL-formula : ex u being LTL-formula st
( u in W & x = 'X' u ) } ;