theorem Th4: :: SYMSP_1:4

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