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 )
hereby :: thesis: ( 'G' F |-0 A implies F |- A )
assume F |- A ; :: thesis: 'G' F |-0 A
then F |= A by LTLAXIO1:41;
hence 'G' F |-0 A by th268, th262b; :: thesis: verum
end;
assume 'G' F |-0 A ; :: thesis: F |- A
then 'G' F |=0 A by th266;
hence F |- A by LTLAXIO4:33, th262b; :: thesis: verum