let A be Element of LTLB_WFF ; :: thesis: for F being Subset of LTLB_WFF holds F |- ('G' A) => ('G' ('X' A))
let F be Subset of LTLB_WFF; :: thesis: F |- ('G' A) => ('G' ('X' A))
{A} |- 'G' ('X' A) by LTLAXIO4:33, th19a;
then F \/ {A} |- 'G' ('X' A) by mon2, XBOOLE_1:7;
hence F |- ('G' A) => ('G' ('X' A)) by LTLAXIO1:57; :: thesis: verum