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