let V be RealLinearSpace; for x, y being VECTOR of st Gen x,y holds
( ( for u, u1, v, v1, w being Element of 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 ex u1 being Element of st
( w <> u1 & w,u1 '//' u,v ) ) & ( for u, v, w being Element of ex u1 being Element of st
( w <> u1 & u,v '//' w,u1 ) ) )
let x, y be VECTOR of ; ( Gen x,y implies ( ( for u, u1, v, v1, w being Element of 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 ex u1 being Element of st
( w <> u1 & w,u1 '//' u,v ) ) & ( for u, v, w being Element of ex u1 being Element of st
( w <> u1 & u,v '//' w,u1 ) ) ) )
assume A1:
Gen x,y
; ( ( for u, u1, v, v1, w being Element of 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 ex u1 being Element of st
( w <> u1 & w,u1 '//' u,v ) ) & ( for u, v, w being Element of ex u1 being Element of st
( w <> u1 & u,v '//' w,u1 ) ) )
set S = CESpace V,x,y;
A2:
CESpace V,x,y = AffinStruct(# the carrier of V,(CORTE V,x,y) #)
by ANALORT:def 7;
thus
for u, u1, v, v1, w being Element of 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 ex u1 being Element of st
( w <> u1 & w,u1 '//' u,v ) ) & ( for u, v, w being Element of ex u1 being Element of st
( w <> u1 & u,v '//' w,u1 ) ) )proof
let u,
u1,
v,
v1,
w be
Element of ;
( 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 u' =
u,
v' =
v,
w' =
w,
u1' =
u1,
v1' =
v1 as
Element of
by A2;
u',
u',
v',
w' are_COrte_wrt x,
y
by ANALORT:20;
hence
u,
u '//' v,
w
by ANALORT:56;
( 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 ) )
u',
v',
w',
w' are_COrte_wrt x,
y
by ANALORT:22;
hence
u,
v '//' w,
w
by ANALORT:56;
( ( 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 ) )
(
u',
v',
u1',
v1' are_COrte_wrt x,
y &
u',
v',
v1',
u1' are_COrte_wrt x,
y & not
u' = v' implies
u1' = v1' )
by A1, ANALORT:30;
hence
(
u,
v '//' u1,
v1 &
u,
v '//' v1,
u1 & not
u = v implies
u1 = v1 )
by ANALORT:56;
( ( 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 ) )
(
u',
v',
u1',
v1' are_COrte_wrt x,
y &
u',
v',
u1',
w' are_COrte_wrt x,
y & not
u',
v',
v1',
w' are_COrte_wrt x,
y implies
u',
v',
w',
v1' 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:56;
( ( 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 ) )
(
u',
v',
u1',
v1' are_COrte_wrt x,
y implies
v',
u',
v1',
u1' are_COrte_wrt x,
y )
by ANALORT:34;
hence
(
u,
v '//' u1,
v1 implies
v,
u '//' v1,
u1 )
by ANALORT:56;
( ( 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 ) )
(
u',
v',
u1',
v1' are_COrte_wrt x,
y &
u',
v',
v1',
w' are_COrte_wrt x,
y implies
u',
v',
u1',
w' 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:56;
( not u,u1 '//' v,v1 or v,v1 '//' u,u1 or v,v1 '//' u1,u )
( not
u',
u1',
v',
v1' are_COrte_wrt x,
y or
v',
v1',
u',
u1' are_COrte_wrt x,
y or
v',
v1',
u1',
u' 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:56;
verum
thus
verum
;
verum
end;
thus
for u, v, w being Element of ex u1 being Element of st
( w <> u1 & w,u1 '//' u,v )
for u, v, w being Element of ex u1 being Element of st
( w <> u1 & u,v '//' w,u1 )proof
let u,
v,
w be
Element of ;
ex u1 being Element of st
( w <> u1 & w,u1 '//' u,v )
reconsider u' =
u,
v' =
v,
w' =
w as
Element of
by A2;
consider u1' being
Element of
such that A3:
w' <> u1'
and A4:
w',
u1',
u',
v' are_COrte_wrt x,
y
by A1, ANALORT:38;
reconsider u1 =
u1' as
Element of
by A2;
w,
u1 '//' u,
v
by A4, ANALORT:56;
hence
ex
u1 being
Element of st
(
w <> u1 &
w,
u1 '//' u,
v )
by A3;
verum
end;
let u, v, w be Element of ; ex u1 being Element of st
( w <> u1 & u,v '//' w,u1 )
reconsider u' = u, v' = v, w' = w as Element of by A2;
consider u1' being Element of such that
A5:
w' <> u1'
and
A6:
u',v',w',u1' are_COrte_wrt x,y
by A1, ANALORT:40;
reconsider u1 = u1' as Element of by A2;
u,v '//' w,u1
by A6, ANALORT:56;
hence
ex u1 being Element of st
( w <> u1 & u,v '//' w,u1 )
by A5; verum