let A be Element of LTLB_WFF ; :: thesis: for F being Subset of LTLB_WFF holds F |- ('G' A) => A

let F be Subset of LTLB_WFF; :: thesis: F |- ('G' A) => A

A1: {A} c= F \/ {A} by XBOOLE_1:7;

A in {A} by TARSKI:def 1;

then F \/ {A} |- A by A1, LTLAXIO1:42;

hence F |- ('G' A) => A by LTLAXIO1:57; :: thesis: verum

let F be Subset of LTLB_WFF; :: thesis: F |- ('G' A) => A

A1: {A} c= F \/ {A} by XBOOLE_1:7;

A in {A} by TARSKI:def 1;

then F \/ {A} |- A by A1, LTLAXIO1:42;

hence F |- ('G' A) => A by LTLAXIO1:57; :: thesis: verum