let F be Field; :: thesis: for S being SymSp of F
for a, b, x being Element of S st not a _|_ holds
a _|_
let S be SymSp of F; :: thesis: for a, b, x being Element of S st not a _|_ holds
a _|_
let a, b, 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, Def2; :: thesis: verum