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