let p, q be Element of LTLB_WFF ; :: thesis:
let F be Subset of LTLB_WFF; :: thesis:
set G = F \/ {p};
assume F \/ {p} |- q ; :: thesis:
then consider f being FinSequence of LTLB_WFF such that
A1: f . (len f) = q and
A2: 1 <= len f and
A3: for i being Nat st 1 <= i & i <= len f holds
prc f,F \/ {p},i ;
defpred S₁[ Nat] means ( 1 <= $1 & $1 <= len f implies F |- ('G' p) => (f /. $1) );
A4: for i being Nat st ( for j being Nat st j < i holds
S₁[j] ) holds
S₁[i]

let i be Nat; :: thesis:
assume A5: for j being Nat st j < i holds
S₁[j] ; :: thesis:

end;

end;

set t = f /. i;
(f /. i) => (('G' p) => (f /. i)) in LTL_axioms by Th34;
then A12: F |- (f /. i) => (('G' p) => (f /. i)) by Th42;
f /. i in F by A6, A7, A11, Lm1;
then F |- f /. i by Th42;
hence F |- ('G' p) => (f /. i) by A12, Th43; :: thesis:

end;

end;

suppose ex j, k being Nat st
( 1 <= j & j < i & 1 <= k & k < i & ( f /. j,f /. k MP_rule f /. i or f /. j,f /. k IND_rule f /. i ) ) ; :: thesis:

then consider j, k being Nat such that
A15: 1 <= j and
A16: j < i and
A17: 1 <= k and
A18: k < i and
A19: ( f /. j,f /. k MP_rule f /. i or f /. j,f /. k IND_rule f /. i ) ;
j <= len f by A7, A16, XXREAL_0:2;
then A20: F |- ('G' p) => (f /. j) by A5, A15, A16;
k <= len f by A7, A18, XXREAL_0:2;
then A21: F |- ('G' p) => (f /. k) by A5, A17, A18;

set t3 = (('G' p) => ((f /. j) => (f /. i))) => ((('G' p) => (f /. j)) => (('G' p) => (f /. i)));
(('G' p) => ((f /. j) => (f /. i))) => ((('G' p) => (f /. j)) => (('G' p) => (f /. i))) in LTL_axioms by Th35;
then A23: F |- (('G' p) => ((f /. j) => (f /. i))) => ((('G' p) => (f /. j)) => (('G' p) => (f /. i))) by Th42;
F |- ('G' p) => ((f /. j) => (f /. i)) by A21, A22;
then F |- (('G' p) => (f /. j)) => (('G' p) => (f /. i)) by A23, Th43;
hence F |- ('G' p) => (f /. i) by A20, Th43; :: thesis:

end;

then consider A, B being Element of LTLB_WFF such that
A24: f /. j = A => B and
A25: f /. k = A => ('X' A) and
A26: f /. i = A => ('G' B) ;
set Gp = 'G' p;
set XGp = 'X' ('G' p);
set XA = 'X' A;
set Xq = 'X' q;
set GB = 'G' B;
('G' p) => (p '&&' ('X' ('G' p))) in LTL_axioms by Def17;
then F |- ('G' p) => (p '&&' ('X' ('G' p))) by Th42;
then A27: F |- ('G' p) => ('X' ('G' p)) by Th46;
F |- (('G' p) '&&' A) => ('X' A) by A21, A25, Th48;
then A28: F |- (('G' p) '&&' A) => (('X' ('G' p)) '&&' ('X' A)) by A27, Th50;
F |- (('X' ('G' p)) '&&' ('X' A)) => ('X' (('G' p) '&&' A)) by Th53;
then A29: F |- (('G' p) '&&' A) => ('X' (('G' p) '&&' A)) by A28, Th47;
F |- (('G' p) '&&' A) => B by A20, A24, Th48;
then F |- (('G' p) '&&' A) => ('G' B) by A29, Th45;
hence F |- ('G' p) => (f /. i) by A26, Th49; :: thesis:

end;

('G' p) => (p '&&' ('X' ('G' p))) in LTL_axioms by Def17;
then F |- ('G' p) => (p '&&' ('X' ('G' p))) by Th42;
then A31: F |- ('G' p) => ('X' ('G' p)) by Th46;
consider j being Nat, q, r being Element of LTLB_WFF such that
A32: 1 <= j and
A33: j < i and
A34: f /. j NEX_rule f /. i by A30;
('X' (('G' p) => (f /. j))) => (('X' ('G' p)) => ('X' (f /. j))) in LTL_axioms by Def17;
then A35: F |- ('X' (('G' p) => (f /. j))) => (('X' ('G' p)) => ('X' (f /. j))) by Th42;
j <= len f by A7, A33, XXREAL_0:2;
then F |- 'X' (('G' p) => (f /. j)) by A5, A32, A33, Th44;
then A36: F |- ('X' ('G' p)) => ('X' (f /. j)) by A35, Th43;
f /. i = 'X' (f /. j) by A34;
hence F |- ('G' p) => (f /. i) by A36, A31, Th47; :: thesis:

end;