theorem Th8: :: SYMSP_1:8

for F being Field
for S being SymSp of F
for a, b, a9, b9 being Element of S st not a _|_ & b _|_ & not b _|_ & a _|_ holds
( not a _|_ & not b _|_ )