let
P
be
PNPair
;
:: thesis:
(
P
=
[
(
<*>
LTLB_WFF
)
,
(
<*>
LTLB_WFF
)
]
implies
P
is
complete
)
assume
A1
:
P
=
[
(
<*>
LTLB_WFF
)
,
(
<*>
LTLB_WFF
)
]
;
:: thesis:
P
is
complete
then
A2
:
rng
(
P
`1
)
=
{}
;
rng
(
P
`2
)
=
{}
by
A1
;
then
tau
(
rng
P
)
=
rng
P
by
A2
;
hence
P
is
complete
;
:: thesis:
verum