let F be Field; :: thesis: for S being SymSp of F
for a, b being Element of S st b _|_ holds
b _|_
let S be SymSp of F; :: thesis: for a, b being Element of S st b _|_ holds
b _|_
let a, b be Element of S; :: thesis: ( b _|_ implies b _|_ )
assume b _|_ ; :: thesis: b _|_
then b _|_ by Def1;
hence b _|_ by VECTSP_1:14; :: thesis: verum