let F be Field; :: thesis: for S being SymSp of F
for b, a, c being Element of S st not a _|_ & a _|_ holds
not a _|_
let S be SymSp of F; :: thesis: for b, a, c being Element of S st not a _|_ & a _|_ holds
not a _|_
let b, a, c be Element of S; :: thesis: ( not a _|_ & a _|_ implies not a _|_ )
assume A1: ( not a _|_ & a _|_ ) ; :: thesis: not a _|_
assume A2: a _|_ ; :: thesis: contradiction
a _|_ by A1, Def1;
then a _|_ by VECTSP_1:59;
then a _|_ by A2, Def1;
then a _|_ by RLVECT_1:def 6;
then a _|_ by RLVECT_1:16;
hence contradiction by A1, RLVECT_1:10; :: thesis: verum