H 'R' G is LTL-formula-like

proof

( H is Element of LTL_WFF & G is Element of LTL_WFF ) by Def13;
hence H 'R' G is Element of LTL_WFF by Def12; :: according to MODELC_2:def 10 :: thesis: verum

end;

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