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