let F be Field; :: thesis: for S being SymSp of F
for b, a, x being Element of S st not a _|_ holds
a _|_
let S be SymSp of F; :: thesis: for b, a, x being Element of S st not a _|_ holds
a _|_
let b, a, x be Element of S; :: thesis: ( not a _|_ implies a _|_ )
assume A1: not a _|_ ; :: thesis: a _|_
then ex l being Element of F st a _|_ by Def1;
hence a _|_ by A1, Def5; :: thesis: verum