let
n
be
Element
of
NAT
;
:: thesis:
for
M
being
LTLModel
holds
(
SAT
M
)
.
[
n
,
TVERUM
]
=
1
let
M
be
LTLModel
;
:: thesis:
(
SAT
M
)
.
[
n
,
TVERUM
]
=
1
assume
not
(
SAT
M
)
.
[
n
,
TVERUM
]
=
1 ;
:: thesis:
contradiction
then
not
(
SAT
M
)
.
[
n
,
TFALSUM
]
=
0
by
Th5
;
hence
contradiction
by
Def11
;
:: thesis:
verum