let V be RealLinearSpace; for x, y being VECTOR of V st Gen x,y holds
( ( for u, u1, v, v1, w 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 ) ) ) & ( 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 ) ) & ( 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 ) ) )
let x, y be VECTOR of V; ( Gen x,y implies ( ( for u, u1, v, v1, w 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 ) ) ) & ( 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 ) ) & ( 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 ) ) ) )
assume A1:
Gen x,y
; ( ( for u, u1, v, v1, w 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 ) ) ) & ( 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 ) ) & ( 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 ) ) )
set S = CMSpace (V,x,y);
A2:
CMSpace (V,x,y) = OrtStr(# the carrier of V,(CORTM (V,x,y)) #)
by ANALORT:def 8;
thus
for u, u1, v, v1, w 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 ) )
( ( 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 ) ) & ( 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 ) ) )proof
let u,
u1,
v,
v1,
w be
Element of
(CMSpace (V,x,y));
( 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 ) )
reconsider u9 =
u,
v9 =
v,
w9 =
w,
u19 =
u1,
v19 =
v1 as
Element of
V by A2;
u9,
u9,
v9,
w9 are_COrtm_wrt x,
y
by ANALORT:21;
hence
u,
u '//' v,
w
by ANALORT:55;
( 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 ) )
u9,
v9,
w9,
w9 are_COrtm_wrt x,
y
by ANALORT:23;
hence
u,
v '//' w,
w
by ANALORT:55;
( ( 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 ) )
(
u9,
v9,
u19,
v19 are_COrtm_wrt x,
y &
u9,
v9,
v19,
u19 are_COrtm_wrt x,
y & not
u9 = v9 implies
u19 = v19 )
by A1, ANALORT:31;
hence
(
u,
v '//' u1,
v1 &
u,
v '//' v1,
u1 & not
u = v implies
u1 = v1 )
by ANALORT:55;
( ( 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 ) )
(
u9,
v9,
u19,
v19 are_COrtm_wrt x,
y &
u9,
v9,
u19,
w9 are_COrtm_wrt x,
y & not
u9,
v9,
v19,
w9 are_COrtm_wrt x,
y implies
u9,
v9,
w9,
v19 are_COrtm_wrt x,
y )
by A1, ANALORT:33;
hence
(
u,
v '//' u1,
v1 &
u,
v '//' u1,
w & not
u,
v '//' v1,
w implies
u,
v '//' w,
v1 )
by ANALORT:55;
( ( 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 ) )
(
u9,
v9,
u19,
v19 are_COrtm_wrt x,
y implies
v9,
u9,
v19,
u19 are_COrtm_wrt x,
y )
by ANALORT:35;
hence
(
u,
v '//' u1,
v1 implies
v,
u '//' v1,
u1 )
by ANALORT:55;
( ( 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 ) )
(
u9,
v9,
u19,
v19 are_COrtm_wrt x,
y &
u9,
v9,
v19,
w9 are_COrtm_wrt x,
y implies
u9,
v9,
u19,
w9 are_COrtm_wrt x,
y )
by A1, ANALORT:37;
hence
(
u,
v '//' u1,
v1 &
u,
v '//' v1,
w implies
u,
v '//' u1,
w )
by ANALORT:55;
( not u,u1 '//' v,v1 or v,v1 '//' u,u1 or v,v1 '//' u1,u )
( not
u9,
u19,
v9,
v19 are_COrtm_wrt x,
y or
v9,
v19,
u9,
u19 are_COrtm_wrt x,
y or
v9,
v19,
u19,
u9 are_COrtm_wrt x,
y )
by A1, ANALORT:19;
hence
( not
u,
u1 '//' v,
v1 or
v,
v1 '//' u,
u1 or
v,
v1 '//' u1,
u )
by ANALORT:55;
verum
end;
thus
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 )
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 )proof
let u,
v,
w be
Element of
(CMSpace (V,x,y));
ex u1 being Element of (CMSpace (V,x,y)) st
( w <> u1 & w,u1 '//' u,v )
reconsider u9 =
u,
v9 =
v,
w9 =
w as
Element of
V by A2;
consider u19 being
Element of
V such that A3:
w9 <> u19
and A4:
w9,
u19,
u9,
v9 are_COrtm_wrt x,
y
by A1, ANALORT:39;
reconsider u1 =
u19 as
Element of
(CMSpace (V,x,y)) by A2;
w,
u1 '//' u,
v
by A4, ANALORT:55;
hence
ex
u1 being
Element of
(CMSpace (V,x,y)) st
(
w <> u1 &
w,
u1 '//' u,
v )
by A3;
verum
end;
let u, v, w be Element of (CMSpace (V,x,y)); ex u1 being Element of (CMSpace (V,x,y)) st
( w <> u1 & u,v '//' w,u1 )
reconsider u9 = u, v9 = v, w9 = w as Element of V by A2;
consider u19 being Element of V such that
A5:
w9 <> u19
and
A6:
u9,v9,w9,u19 are_COrtm_wrt x,y
by A1, ANALORT:41;
reconsider u1 = u19 as Element of (CMSpace (V,x,y)) by A2;
u,v '//' w,u1
by A6, ANALORT:55;
hence
ex u1 being Element of (CMSpace (V,x,y)) st
( w <> u1 & u,v '//' w,u1 )
by A5; verum