let A, B be Element of LTLB_WFF ; :: thesis: for F being Subset of LTLB_WFF holds F |- ('G' (A => B)) => (('G' (A => ('X' A))) => ('G' (A => ('G' B))))
let F be Subset of LTLB_WFF; :: thesis: F |- ('G' (A => B)) => (('G' (A => ('X' A))) => ('G' (A => ('G' B))))
A => B in {(A => B)} by TARSKI:def 1;
then A => B in F \/ {(A => B)} by XBOOLE_0:def 3;
then A => B in (F \/ {(A => B)}) \/ {(A => ('X' A))} by XBOOLE_0:def 3;
then A1: (F \/ {(A => B)}) \/ {(A => ('X' A))} |- A => B by LTLAXIO1:42;
A => ('X' A) in {(A => ('X' A))} by TARSKI:def 1;
then A => ('X' A) in (F \/ {(A => B)}) \/ {(A => ('X' A))} by XBOOLE_0:def 3;
then (F \/ {(A => B)}) \/ {(A => ('X' A))} |- A => ('X' A) by LTLAXIO1:42;
then (F \/ {(A => B)}) \/ {(A => ('X' A))} |- 'G' (A => ('G' B)) by LTLAXIO1:45, LTLAXIO1:54, A1;
then F \/ {(A => B)} |- ('G' (A => ('X' A))) => ('G' (A => ('G' B))) by LTLAXIO1:57;
hence F |- ('G' (A => B)) => (('G' (A => ('X' A))) => ('G' (A => ('G' B)))) by LTLAXIO1:57; :: thesis: verum