let R be domRing; :: thesis: for a being non zero Element of R holds support (BRoots (a | R)) = {}
let a be non zero Element of R; :: thesis: support (BRoots (a | R)) = {}

now :: thesis: ( support (BRoots (a | R)) <> {} implies for b being Element of support (BRoots (a | R)) holds contradiction )

assume A: support (BRoots (a | R)) <> {} ; :: thesis: for b being Element of support (BRoots (a | R)) holds contradiction
let b be Element of support (BRoots (a | R)); :: thesis: contradiction
b in Roots (a | R) by A, UPROOTS:def 9;
hence contradiction ; :: thesis: verum

end;

hence support (BRoots (a | R)) = {} ; :: thesis: verum