theorem Th10: :: SYMSP_1:10

for F being Field
for S being SymSp of F
for a, b, c being Element of S st (1_ F) + (1_ F) <> 0. F & a <> 0. S & b <> 0. S & c <> 0. S holds
ex p being Element of S st
( not a _|_ & not b _|_ & not c _|_ )