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

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