let V be RealLinearSpace; :: thesis: for x, y being VECTOR of V st Gen x,y holds
CMSpace (V,x,y) is Oriented_Orthogonality_Space
let x, y be VECTOR of V; :: thesis: ( Gen x,y implies CMSpace (V,x,y) is Oriented_Orthogonality_Space )
assume A1: Gen x,y ; :: thesis: CMSpace (V,x,y) is Oriented_Orthogonality_Space
then A2: for u, v, w being Element of (CMSpace (V,x,y)) ex u1 being Element of (CMSpace (V,x,y)) st
( w <> u1 & w,u1 '//' u,v ) by Th2;
A3: for u, v, w being Element of (CMSpace (V,x,y)) ex u1 being Element of (CMSpace (V,x,y)) st
( w <> u1 & u,v '//' w,u1 ) by A1, Th2;
for u, u1, v, v1, w, w1, w2 being Element of (CMSpace (V,x,y)) 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 ) ) by A1, Th2;
hence CMSpace (V,x,y) is Oriented_Orthogonality_Space by A2, A3, Def1; :: thesis: verum