consider
a
being
Element
of
R
such that
A1
: (
a
<>
1.
R
&
a
<>
0.
R
)
by
Def1
;
take
a
;
:: thesis:
not
a
is
trivial
thus
not
a
is
trivial
by
A1
;
:: thesis:
verum