:: deftheorem Def1 defines OrtSp-like ORTSP_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 OrtSp-like iff for a, b, c, d, x being Element of IT
for l being Element of F holds
( ( a <> 0. IT & b <> 0. IT & c <> 0. IT & d <> 0. IT implies ex p being Element of IT st
( not a _|_ & not b _|_ & not c _|_ & not d _|_ ) ) & ( 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 _|_ ) ) );