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