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