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