theorem Th3: :: SYMSP_1:3

for F being Field
for S being SymSp of F
for a, b, c being Element of S st not b _|_ & b _|_ holds
not b _|_