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

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