let
a
,
x
be
Element
of
Benzene
;
:: thesis:
(
a
=
0
implies
a
"\/"
x
=
x
)
assume
a
=
0
;
:: thesis:
a
"\/"
x
=
x
then
a
c=
x
;
then
a
[=
x
by
Th24
;
hence
a
"\/"
x
=
x
;
:: thesis:
verum