'X' H is LTL-formula-like

proof

H is Element of LTL_WFF by Def13;
hence 'X' H is Element of LTL_WFF by Def12; :: according to MODELC_2:def 10 :: thesis: verum

end;

hence 'X' H is LTL-formula-like ; :: thesis: verum