let A be Element of LTLB_WFF ; :: thesis: for F being finite Subset of LTLB_WFF holds

( F |- A iff 'G' F |-0 A )

let F be finite Subset of LTLB_WFF; :: thesis: ( F |- A iff 'G' F |-0 A )

then 'G' F |=0 A by th266;

hence F |- A by LTLAXIO4:33, th262b; :: thesis: verum

( F |- A iff 'G' F |-0 A )

let F be finite Subset of LTLB_WFF; :: thesis: ( F |- A iff 'G' F |-0 A )

hereby :: thesis: ( 'G' F |-0 A implies F |- A )

assume
'G' F |-0 A
; :: thesis: F |- Aassume
F |- A
; :: thesis: 'G' F |-0 A

then F |= A by LTLAXIO1:41;

hence 'G' F |-0 A by th268, th262b; :: thesis: verum

end;then F |= A by LTLAXIO1:41;

hence 'G' F |-0 A by th268, th262b; :: thesis: verum

then 'G' F |=0 A by th266;

hence F |- A by LTLAXIO4:33, th262b; :: thesis: verum