:: deftheorem Def1 defines SymSp-like SYMSP_1:def 1 :
for F being Field
for IT being non empty right_complementable Abelian add-associative right_zeroed SymStr over F holds
( IT is SymSp-like iff for a, b, c, x being Element of IT
for l being Element of F holds
( ( a <> 0. IT implies ex y being Element of IT st not a _|_ ) & ( b _|_ implies b _|_ ) & ( a _|_ & a _|_ implies a _|_ ) & ( not a _|_ implies ex k being Element of F st a _|_ ) & ( b + c _|_ & c + a _|_ implies a + b _|_ ) ) );