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