let
A
be
QC-alphabet
;
:: thesis:
for
p
being
Element
of
CQC-WFF
A
holds
p
=>
p
in
TAUT
A
let
p
be
Element
of
CQC-WFF
A
;
:: thesis:
p
=>
p
in
TAUT
A
(
(
(
'not'
p
)
=>
p
)
=>
p
in
TAUT
A
&
p
=>
(
(
'not'
p
)
=>
p
)
in
TAUT
A
)
by
CQC_THE1:42
,
CQC_THE1:43
;
hence
p
=>
p
in
TAUT
A
by
Th3
;
:: thesis:
verum