theorem Th2: :: SYMSP_1:2

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