:: deftheorem Def1 defines Oriented_Orthogonality_Space-like DIRORT:def 1 :
for IT being non empty OrtStr holds
( IT is Oriented_Orthogonality_Space-like iff ( ( for u, u1, v, v1, w being Element of IT holds
( u,u '//' v,w & u,v '//' w,w & ( u,v '//' u1,v1 & u,v '//' v1,u1 & not u = v implies u1 = v1 ) & ( u,v '//' u1,v1 & u,v '//' u1,w & not u,v '//' v1,w implies u,v '//' w,v1 ) & ( u,v '//' u1,v1 implies v,u '//' v1,u1 ) & ( u,v '//' u1,v1 & u,v '//' v1,w implies u,v '//' u1,w ) & ( not u,u1 '//' v,v1 or v,v1 '//' u,u1 or v,v1 '//' u1,u ) ) ) & ( for u, v, w being Element of IT ex u1 being Element of IT st
( w <> u1 & w,u1 '//' u,v ) ) & ( for u, v, w being Element of IT ex u1 being Element of IT st
( w <> u1 & u,v '//' w,u1 ) ) ) );