theorem
for
V being
RealLinearSpace for
x,
y being
VECTOR of
V st
Gen x,
y holds
ex
u,
v,
w being
VECTOR of
V st
(
u,
v,
u,
w are_COrtm_wrt x,
y & ( for
v1,
w1 being
VECTOR of
V holds
( not
v1,
w1,
u,
v are_COrtm_wrt x,
y or ( not
v1,
w1,
u,
w are_COrtm_wrt x,
y & not
v1,
w1,
w,
u are_COrtm_wrt x,
y ) or
v1 = w1 ) ) )