let F be Field; :: thesis: for S being SymSp of F
for a, b, c being Element of S st not b _|_ & b _|_ holds
not b _|_
let S be SymSp of F; :: thesis: for a, b, c being Element of S st not b _|_ & b _|_ holds
not b _|_
let a, b, c be Element of S; :: thesis: ( not b _|_ & b _|_ implies not b _|_ )
assume that
A1: not b _|_ and
A2: b _|_ ; :: thesis: not b _|_
assume b _|_ ; :: thesis: contradiction
then b _|_ by Def1;
then b _|_ by VECTSP_1:14;
then b _|_ by A2, Def1;
then b _|_ by RLVECT_1:def 3;
then b _|_ by RLVECT_1:5;
hence contradiction by A1, RLVECT_1:4; :: thesis: verum