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