let A be Element of LTLB_WFF ; :: thesis: for F being Subset of LTLB_WFF st F |-0 'G' A holds
F |-0 A
let F be Subset of LTLB_WFF; :: thesis: ( F |-0 'G' A implies F |-0 A )
assume F |-0 'G' A ; :: thesis: F |-0 A
then consider f being FinSequence of LTLB_WFF such that
A1: f . (len f) = 'G' A and
A2: 1 <= len f and
A3: for i being Nat st 1 <= i & i <= len f holds
prc0 f,F,i ;
set g = f ^ <*A*>;
A4: len (f ^ <*A*>) = (len f) + (len <*A*>) by FINSEQ_1:22
.= (len f) + 1 by FINSEQ_1:39 ;
then A5: len f < len (f ^ <*A*>) by NAT_1:16;
then A6: (f ^ <*A*>) /. (len f) = (f ^ <*A*>) . (len f) by A2, Lm1
.= 'G' A by A1, A2, FINSEQ_1:64 ;
1 <= len (f ^ <*A*>) by A2, A4, NAT_1:16;
then (f ^ <*A*>) /. (len (f ^ <*A*>)) = (f ^ <*A*>) . (len (f ^ <*A*>)) by Lm1
.= A by A4, FINSEQ_1:42 ;
then (f ^ <*A*>) /. (len f) REFL0_rule (f ^ <*A*>) /. (len (f ^ <*A*>)) by A6;
then prc0 f ^ <*A*>,F, len (f ^ <*A*>) by A2, A5;
hence F |-0 A by A2, A3, Th40; :: thesis: verum