theorem Th1:
for
V being
RealLinearSpace for
x,
y being
VECTOR of
V st
Gen x,
y holds
( ( for
u,
u1,
v,
v1,
w 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 ) ) ) & ( 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 ) ) & ( 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 ) ) )