let
R
be
domRing
;
:: thesis:
for
a
being non
zero
Element
of
R
holds
card
(
BRoots
(
a

R
)
)
=
0
let
a
be non
zero
Element
of
R
;
:: thesis:
card
(
BRoots
(
a

R
)
)
=
0
support
(
BRoots
(
a

R
)
)
=
{}
by
BR3
;
hence
card
(
BRoots
(
a

R
)
)
=
0
by
bag1a
;
:: thesis:
verum