let A be Element of LTLB_WFF ; :: thesis: for F being finite Subset of LTLB_WFF st F |-0 'G' A holds
F |- A
let F be finite Subset of LTLB_WFF; :: thesis: ( F |-0 'G' A implies F |- A )
assume F |-0 'G' A ; :: thesis: F |- A
then F |=0 'G' A by th266;
hence F |- A by LTLAXIO4:33, th21; :: thesis: verum