let V be RealLinearSpace; :: thesis: 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; :: thesis: ( 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
; :: thesis: ( ( 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 = AffinStruct(# 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 ) )
:: thesis: ( ( 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);
:: thesis: ( 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
V by A2;
thus
u,
u '//' v,
w
:: thesis: ( 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 ) )
thus
u,
v '//' w,
w
:: thesis: ( ( 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 ) )
thus
(
u,
v '//' u1,
v1 &
u,
v '//' v1,
u1 & not
u = v implies
u1 = v1 )
:: thesis: ( ( 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 ) )proof
(
u',
v',
u1',
v1' are_COrtm_wrt x,
y &
u',
v',
v1',
u1' are_COrtm_wrt x,
y & not
u' = v' implies
u1' = v1' )
by A1, ANALORT:31;
hence
(
u,
v '//' u1,
v1 &
u,
v '//' v1,
u1 & not
u = v implies
u1 = v1 )
by ANALORT:57;
:: thesis: verum
end;
thus
(
u,
v '//' u1,
v1 &
u,
v '//' u1,
w & not
u,
v '//' v1,
w implies
u,
v '//' w,
v1 )
:: thesis: ( ( 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 ) )proof
(
u',
v',
u1',
v1' are_COrtm_wrt x,
y &
u',
v',
u1',
w' are_COrtm_wrt x,
y & not
u',
v',
v1',
w' are_COrtm_wrt x,
y implies
u',
v',
w',
v1' 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:57;
:: thesis: verum
end;
thus
(
u,
v '//' u1,
v1 implies
v,
u '//' v1,
u1 )
:: thesis: ( ( 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 ) )proof
(
u',
v',
u1',
v1' are_COrtm_wrt x,
y implies
v',
u',
v1',
u1' are_COrtm_wrt x,
y )
by ANALORT:35;
hence
(
u,
v '//' u1,
v1 implies
v,
u '//' v1,
u1 )
by ANALORT:57;
:: thesis: verum
end;
thus
(
u,
v '//' u1,
v1 &
u,
v '//' v1,
w implies
u,
v '//' u1,
w )
:: thesis: ( not u,u1 '//' v,v1 or v,v1 '//' u,u1 or v,v1 '//' u1,u )proof
(
u',
v',
u1',
v1' are_COrtm_wrt x,
y &
u',
v',
v1',
w' are_COrtm_wrt x,
y implies
u',
v',
u1',
w' 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:57;
:: thesis: verum
end;
thus
( not
u,
u1 '//' v,
v1 or
v,
v1 '//' u,
u1 or
v,
v1 '//' u1,
u )
:: thesis: verumproof
( not
u',
u1',
v',
v1' are_COrtm_wrt x,
y or
v',
v1',
u',
u1' are_COrtm_wrt x,
y or
v',
v1',
u1',
u' 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:57;
:: thesis: verum
end;
thus
verum
;
:: thesis: 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 )
:: thesis: 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);
:: thesis: ex u1 being Element of (CMSpace V,x,y) st
( w <> u1 & w,u1 '//' u,v )
reconsider u' =
u,
v' =
v,
w' =
w as
Element of
V by A2;
consider u1' being
Element of
V such that A3:
(
w' <> u1' &
w',
u1',
u',
v' are_COrtm_wrt x,
y )
by A1, ANALORT:39;
reconsider u1 =
u1' as
Element of
(CMSpace V,x,y) by A2;
(
w <> u1 &
w,
u1 '//' u,
v )
by A3, ANALORT:57;
hence
ex
u1 being
Element of
(CMSpace V,x,y) st
(
w <> u1 &
w,
u1 '//' u,
v )
;
:: thesis: verum
end;
let u, v, w be Element of (CMSpace V,x,y); :: thesis: ex u1 being Element of (CMSpace V,x,y) st
( w <> u1 & u,v '//' w,u1 )
reconsider u' = u, v' = v, w' = w as Element of V by A2;
consider u1' being Element of V such that
A4:
( w' <> u1' & u',v',w',u1' are_COrtm_wrt x,y )
by A1, ANALORT:41;
reconsider u1 = u1' as Element of (CMSpace V,x,y) by A2;
( w <> u1 & u,v '//' w,u1 )
by A4, ANALORT:57;
hence
ex u1 being Element of (CMSpace V,x,y) st
( w <> u1 & u,v '//' w,u1 )
; :: thesis: verum