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