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 (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 ) ) )
let x, y be VECTOR of V; ( Gen x,y implies ( ( 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 ) ) ) )
assume A1:
Gen x,y
; ( ( 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 ) ) )
set S = CESpace (V,x,y);
A2:
CESpace (V,x,y) = OrtStr(# the carrier of V,(CORTE (V,x,y)) #)
by ANALORT:def 7;
thus
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 ) ) )proof
let u,
u1,
v,
v1,
w be
Element of
(CESpace (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_COrte_wrt x,
y
by ANALORT:20;
hence
u,
u '//' v,
w
by ANALORT:54;
( 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_COrte_wrt x,
y
by ANALORT:22;
hence
u,
v '//' w,
w
by ANALORT:54;
( ( 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_COrte_wrt x,
y &
u9,
v9,
v19,
u19 are_COrte_wrt x,
y & not
u9 = v9 implies
u19 = v19 )
by A1, ANALORT:30;
hence
(
u,
v '//' u1,
v1 &
u,
v '//' v1,
u1 & not
u = v implies
u1 = v1 )
by ANALORT:54;
( ( 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_COrte_wrt x,
y &
u9,
v9,
u19,
w9 are_COrte_wrt x,
y & not
u9,
v9,
v19,
w9 are_COrte_wrt x,
y implies
u9,
v9,
w9,
v19 are_COrte_wrt x,
y )
by A1, ANALORT:32;
hence
(
u,
v '//' u1,
v1 &
u,
v '//' u1,
w & not
u,
v '//' v1,
w implies
u,
v '//' w,
v1 )
by ANALORT:54;
( ( 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_COrte_wrt x,
y implies
v9,
u9,
v19,
u19 are_COrte_wrt x,
y )
by ANALORT:34;
hence
(
u,
v '//' u1,
v1 implies
v,
u '//' v1,
u1 )
by ANALORT:54;
( ( 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_COrte_wrt x,
y &
u9,
v9,
v19,
w9 are_COrte_wrt x,
y implies
u9,
v9,
u19,
w9 are_COrte_wrt x,
y )
by A1, ANALORT:36;
hence
(
u,
v '//' u1,
v1 &
u,
v '//' v1,
w implies
u,
v '//' u1,
w )
by ANALORT:54;
( not u,u1 '//' v,v1 or v,v1 '//' u,u1 or v,v1 '//' u1,u )
( not
u9,
u19,
v9,
v19 are_COrte_wrt x,
y or
v9,
v19,
u9,
u19 are_COrte_wrt x,
y or
v9,
v19,
u19,
u9 are_COrte_wrt x,
y )
by A1, ANALORT:18;
hence
( not
u,
u1 '//' v,
v1 or
v,
v1 '//' u,
u1 or
v,
v1 '//' u1,
u )
by ANALORT:54;
verum
end;
thus
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 )proof
let u,
v,
w be
Element of
(CESpace (V,x,y));
ex u1 being Element of (CESpace (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_COrte_wrt x,
y
by A1, ANALORT:38;
reconsider u1 =
u19 as
Element of
(CESpace (V,x,y)) by A2;
w,
u1 '//' u,
v
by A4, ANALORT:54;
hence
ex
u1 being
Element of
(CESpace (V,x,y)) st
(
w <> u1 &
w,
u1 '//' u,
v )
by A3;
verum
end;
let u, v, w be Element of (CESpace (V,x,y)); ex u1 being Element of (CESpace (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_COrte_wrt x,y
by A1, ANALORT:40;
reconsider u1 = u19 as Element of (CESpace (V,x,y)) by A2;
u,v '//' w,u1
by A6, ANALORT:54;
hence
ex u1 being Element of (CESpace (V,x,y)) st
( w <> u1 & u,v '//' w,u1 )
by A5; verum