let
a
,
b
,
c
be
boolean
object
;
:: thesis:
(
a
=>
(
b
'&'
c
)
)
=>
(
a
=>
b
)
=
1
A1
: (
b
=
0
or
b
=
1 )
by
XBOOLEAN:def 3
;
(
a
=
0
or
a
=
1 )
by
XBOOLEAN:def 3
;
hence
(
a
=>
(
b
'&'
c
)
)
=>
(
a
=>
b
)
=
1
by
A1
;
:: thesis:
verum