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