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