theorem Th7: :: SYMSP_1:7

for F being Field
for S being SymSp of F
for a, b, c being Element of S holds
( c _|_ or not c _|_ or not c _|_ )