consider V being RealLinearSpace, x, y being VECTOR of V such that
A1: Gen x,y by ANALMETR:3;
take C = CESpace (V,x,y); :: thesis: C is Oriented_Orthogonality_Space-like
thus ( ( for u, u1, v, v1, w being Element of C 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 C ex u1 being Element of C st
( w <> u1 & w,u1 '//' u,v ) ) & ( for u, v, w being Element of C ex u1 being Element of C st
( w <> u1 & u,v '//' w,u1 ) ) ) by A1, Th1; :: according to DIRORT:def 1 :: thesis: verum