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

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