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