let
p
,
q
be
boolean
object
;
:: thesis:
p
=>
(
p
<=>
q
)
=
p
=>
(
p
=>
q
)
(
p
=
FALSE
or
p
=
TRUE
)
by
Def3
;
hence
p
=>
(
p
<=>
q
)
=
p
=>
(
p
=>
q
)
;
:: thesis:
verum