( H is Element of LTL_WFF & G is Element of LTL_WFF ) by Def10;
then H 'R' G is Element of LTL_WFF by Def9;
hence H 'R' G is LTL-formula-like ; :: thesis: verum