:: DIRORT semantic presentation

begin


notation
let AS be non empty AffinStruct ;
let a, b, c, d be Element of AS;
synonym a,b '//' c,d for a,b // c,d;
end;

theorem Th1: :: DIRORT:1
for V being 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 ) ) )
proof
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 (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; ::_thesis: ( 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 ; ::_thesis: ( ( 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) = AffinStruct(# 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 ) ) ::_thesis: ( ( 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)); ::_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 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; ::_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 ) )
 u9,v9,w9,w9 are_COrte_wrt x,y by ANALORT:22;
hence  u,v '//' w,w by ANALORT:54; ::_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 ) )
 ( 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; ::_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 ) )
 ( 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; ::_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 ) )
 ( 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; ::_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 ) )
 ( 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; ::_thesis: ( 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; ::_thesis: 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 ) ::_thesis: 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)); ::_thesis: 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; ::_thesis: verum
end;
let u, v, w be Element of (CESpace (V,x,y)); ::_thesis: 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; ::_thesis: verum
end;

theorem Th2: :: DIRORT:2
for V being 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 ) ) )
proof
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 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; ::_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 ) )
 u9,v9,w9,w9 are_COrtm_wrt x,y by ANALORT:23;
hence  u,v '//' w,w by ANALORT:55; ::_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 ) )
 ( 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; ::_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 ) )
 ( 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; ::_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 ) )
 ( 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; ::_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 ) )
 ( 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; ::_thesis: ( 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; ::_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 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; ::_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 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; ::_thesis: verum
end;

definition
let IT be non empty AffinStruct ;
attrIT is Oriented_Orthogonality_Space-like  means :Def1: :: DIRORT:def 1
( ( for u, u1, v, v1, w being Element of IT 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 IT ex u1 being Element of IT st
( w <> u1 & w,u1 '//' u,v ) ) & ( for u, v, w being Element of IT ex u1 being Element of IT st
( w <> u1 & u,v '//' w,u1 ) ) );
end;

:: deftheorem Def1 defines Oriented_Orthogonality_Space-like DIRORT:def_1_:_
 for IT being non empty AffinStruct holds
( IT is Oriented_Orthogonality_Space-like iff ( ( for u, u1, v, v1, w being Element of IT 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 IT ex u1 being Element of IT st
( w <> u1 & w,u1 '//' u,v ) ) & ( for u, v, w being Element of IT ex u1 being Element of IT st
( w <> u1 & u,v '//' w,u1 ) ) ) );

registration
cluster non empty Oriented_Orthogonality_Space-like for AffinStruct ;
existence
 ex b1 being non empty AffinStruct st b1 is Oriented_Orthogonality_Space-like
proof
consider V being RealLinearSpace, x, y being VECTOR of V such that
A1: Gen x,y by ANALMETR:3;
take C = CESpace (V,x,y); ::_thesis: C is Oriented_Orthogonality_Space-like
thus  ( ( for u, u1, v, v1, w being Element of C 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 C ex u1 being Element of C st
( w <> u1 & w,u1 '//' u,v ) ) & ( for u, v, w being Element of C ex u1 being Element of C st
( w <> u1 & u,v '//' w,u1 ) ) ) by A1, Th1; :: according to DIRORT:def_1 ::_thesis: verum
end;
end;

definition
mode Oriented_Orthogonality_Space is non empty Oriented_Orthogonality_Space-like AffinStruct ;
end;

theorem Th3: :: DIRORT:3
for V being RealLinearSpace
for x, y being VECTOR of V st Gen x,y holds
CMSpace (V,x,y) is Oriented_Orthogonality_Space
proof
let V be RealLinearSpace; ::_thesis: for x, y being VECTOR of V st Gen x,y holds
CMSpace (V,x,y) is Oriented_Orthogonality_Space
let x, y be VECTOR of V; ::_thesis: ( Gen x,y implies CMSpace (V,x,y) is Oriented_Orthogonality_Space )
assume A1: Gen x,y ; ::_thesis: CMSpace (V,x,y) is Oriented_Orthogonality_Space
then A2: 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 ) by Th2;
A3: 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 ) by A1, Th2;
 for u, u1, v, v1, w, w1, w2 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 ) ) by A1, Th2;
hence  CMSpace (V,x,y) is Oriented_Orthogonality_Space by A2, A3, Def1; ::_thesis: verum
end;

theorem Th4: :: DIRORT:4
for V being RealLinearSpace
for x, y being VECTOR of V st Gen x,y holds
CESpace (V,x,y) is Oriented_Orthogonality_Space
proof
let V be RealLinearSpace; ::_thesis: for x, y being VECTOR of V st Gen x,y holds
CESpace (V,x,y) is Oriented_Orthogonality_Space
let x, y be VECTOR of V; ::_thesis: ( Gen x,y implies CESpace (V,x,y) is Oriented_Orthogonality_Space )
assume A1: Gen x,y ; ::_thesis: CESpace (V,x,y) is Oriented_Orthogonality_Space
then A2: 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 ) by Th1;
A3: 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 ) by A1, Th1;
 for u, u1, v, v1, w, w1, w2 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 ) ) by A1, Th1;
hence  CESpace (V,x,y) is Oriented_Orthogonality_Space by A2, A3, Def1; ::_thesis: verum
end;


theorem :: DIRORT:5
for AS being Oriented_Orthogonality_Space
for u, v, w being Element of AS ex u1 being Element of AS st
( u1,w '//' u,v & u1 <> w )
proof
let AS be Oriented_Orthogonality_Space; ::_thesis: for u, v, w being Element of AS ex u1 being Element of AS st
( u1,w '//' u,v & u1 <> w )
let u, v, w be Element of AS; ::_thesis: ex u1 being Element of AS st
( u1,w '//' u,v & u1 <> w )
consider u1 being Element of AS such that
A1: u1 <> w and
A2: w,u1 '//' v,u by Def1;
 u1,w '//' u,v by A2, Def1;
hence  ex u1 being Element of AS st
( u1,w '//' u,v & u1 <> w ) by A1; ::_thesis: verum
end;

theorem :: DIRORT:6
for AS being Oriented_Orthogonality_Space
for u, v, w being Element of AS ex u1 being Element of AS st
( u <> u1 & ( v,w '//' u,u1 or v,w '//' u1,u ) )
proof
let AS be Oriented_Orthogonality_Space; ::_thesis: for u, v, w being Element of AS ex u1 being Element of AS st
( u <> u1 & ( v,w '//' u,u1 or v,w '//' u1,u ) )
let u, v, w be Element of AS; ::_thesis: ex u1 being Element of AS st
( u <> u1 & ( v,w '//' u,u1 or v,w '//' u1,u ) )
consider u1 being Element of AS such that
A1: u <> u1 and
A2: u,u1 '//' v,w by Def1;
 ( v,w '//' u,u1 or v,w '//' u1,u ) by A2, Def1;
hence  ex u1 being Element of AS st
( u <> u1 & ( v,w '//' u,u1 or v,w '//' u1,u ) ) by A1; ::_thesis: verum
end;

definition
let AS be Oriented_Orthogonality_Space;
let a, b, c, d be Element of AS;
preda,b _|_ c,d means :: DIRORT:def 2
( a,b '//' c,d or a,b '//' d,c );
end;

:: deftheorem  defines _|_ DIRORT:def_2_:_
 for AS being Oriented_Orthogonality_Space
for a, b, c, d being Element of AS holds
( a,b _|_ c,d iff ( a,b '//' c,d or a,b '//' d,c ) );

definition
let AS be Oriented_Orthogonality_Space;
let a, b, c, d be Element of AS;
preda,b // c,d means :Def3: :: DIRORT:def 3
 ex e, f being Element of AS st
( e <> f & e,f '//' a,b & e,f '//' c,d );
end;

:: deftheorem Def3 defines // DIRORT:def_3_:_
 for AS being Oriented_Orthogonality_Space
for a, b, c, d being Element of AS holds
( a,b // c,d iff ex e, f being Element of AS st
( e <> f & e,f '//' a,b & e,f '//' c,d ) );

definition
let IT be Oriented_Orthogonality_Space;
attrIT is bach_transitive  means :Def4: :: DIRORT:def 4
 for u, u1, u2, v, v1, v2, w, w1 being Element of IT st u,u1 '//' v,v1 & w,w1 '//' v,v1 & w,w1 '//' u2,v2 & not w = w1 & not v = v1 holds
u,u1 '//' u2,v2;
end;

:: deftheorem Def4 defines bach_transitive DIRORT:def_4_:_
 for IT being Oriented_Orthogonality_Space holds
( IT is bach_transitive iff for u, u1, u2, v, v1, v2, w, w1 being Element of IT st u,u1 '//' v,v1 & w,w1 '//' v,v1 & w,w1 '//' u2,v2 & not w = w1 & not v = v1 holds
u,u1 '//' u2,v2 );

definition
let IT be Oriented_Orthogonality_Space;
attrIT is right_transitive  means :Def5: :: DIRORT:def 5
 for u, u1, u2, v, v1, v2, w, w1 being Element of IT st u,u1 '//' v,v1 & v,v1 '//' w,w1 & u2,v2 '//' w,w1 & not w = w1 & not v = v1 holds
u,u1 '//' u2,v2;
end;

:: deftheorem Def5 defines right_transitive DIRORT:def_5_:_
 for IT being Oriented_Orthogonality_Space holds
( IT is right_transitive iff for u, u1, u2, v, v1, v2, w, w1 being Element of IT st u,u1 '//' v,v1 & v,v1 '//' w,w1 & u2,v2 '//' w,w1 & not w = w1 & not v = v1 holds
u,u1 '//' u2,v2 );

definition
let IT be Oriented_Orthogonality_Space;
attrIT is left_transitive  means :Def6: :: DIRORT:def 6
 for u, u1, u2, v, v1, v2, w, w1 being Element of IT st u,u1 '//' v,v1 & v,v1 '//' w,w1 & u,u1 '//' u2,v2 & not u = u1 & not v = v1 holds
u2,v2 '//' w,w1;
end;

:: deftheorem Def6 defines left_transitive DIRORT:def_6_:_
 for IT being Oriented_Orthogonality_Space holds
( IT is left_transitive iff for u, u1, u2, v, v1, v2, w, w1 being Element of IT st u,u1 '//' v,v1 & v,v1 '//' w,w1 & u,u1 '//' u2,v2 & not u = u1 & not v = v1 holds
u2,v2 '//' w,w1 );

definition
let IT be Oriented_Orthogonality_Space;
attrIT is Euclidean_like  means :Def7: :: DIRORT:def 7
 for u, u1, v, v1 being Element of IT st u,u1 '//' v,v1 holds
v,v1 '//' u1,u;
end;

:: deftheorem Def7 defines Euclidean_like DIRORT:def_7_:_
 for IT being Oriented_Orthogonality_Space holds
( IT is Euclidean_like iff for u, u1, v, v1 being Element of IT st u,u1 '//' v,v1 holds
v,v1 '//' u1,u );

definition
let IT be Oriented_Orthogonality_Space;
attrIT is Minkowskian_like  means :Def8: :: DIRORT:def 8
 for u, u1, v, v1 being Element of IT st u,u1 '//' v,v1 holds
v,v1 '//' u,u1;
end;

:: deftheorem Def8 defines Minkowskian_like DIRORT:def_8_:_
 for IT being Oriented_Orthogonality_Space holds
( IT is Minkowskian_like iff for u, u1, v, v1 being Element of IT st u,u1 '//' v,v1 holds
v,v1 '//' u,u1 );

theorem :: DIRORT:7
for AS being Oriented_Orthogonality_Space
for u, u1, w being Element of AS holds
( u,u1 // w,w & w,w // u,u1 )
proof
let AS be Oriented_Orthogonality_Space; ::_thesis: for u, u1, w being Element of AS holds
( u,u1 // w,w & w,w // u,u1 )
let u, u1, w be Element of AS; ::_thesis: ( u,u1 // w,w & w,w // u,u1 )
set v = the Element of AS;
consider v1 being Element of AS such that
A1: v1 <> the Element of AS and
A2: the Element of AS,v1 '//' u,u1 by Def1;
 the Element of AS,v1 '//' w,w by Def1;
hence  ( u,u1 // w,w & w,w // u,u1 ) by A1, A2, Def3; ::_thesis: verum
end;

theorem :: DIRORT:8
for AS being Oriented_Orthogonality_Space
for u, u1, v, v1 being Element of AS st u,u1 // v,v1 holds
v,v1 // u,u1
proof
let AS be Oriented_Orthogonality_Space; ::_thesis: for u, u1, v, v1 being Element of AS st u,u1 // v,v1 holds
v,v1 // u,u1
let u, u1, v, v1 be Element of AS; ::_thesis: ( u,u1 // v,v1 implies v,v1 // u,u1 )
assume  u,u1 // v,v1 ; ::_thesis: v,v1 // u,u1
then  ex w, w1 being Element of AS st
( w <> w1 & w,w1 '//' u,u1 & w,w1 '//' v,v1 ) by Def3;
hence  v,v1 // u,u1 by Def3; ::_thesis: verum
end;

theorem :: DIRORT:9
for AS being Oriented_Orthogonality_Space
for u, u1, v, v1 being Element of AS st u,u1 // v,v1 holds
u1,u // v1,v
proof
let AS be Oriented_Orthogonality_Space; ::_thesis: for u, u1, v, v1 being Element of AS st u,u1 // v,v1 holds
u1,u // v1,v
let u, u1, v, v1 be Element of AS; ::_thesis: ( u,u1 // v,v1 implies u1,u // v1,v )
assume  u,u1 // v,v1 ; ::_thesis: u1,u // v1,v
then consider w, w1 being Element of AS such that
A1: w <> w1 and
A2: w,w1 '//' u,u1 and
A3: w,w1 '//' v,v1 by Def3;
A4: w1,w '//' v1,v by A3, Def1;
 w1,w '//' u1,u by A2, Def1;
hence  u1,u // v1,v by A1, A4, Def3; ::_thesis: verum
end;

theorem :: DIRORT:10
for AS being Oriented_Orthogonality_Space holds
( AS is left_transitive iff for v, v1, w, w1, u2, v2 being Element of AS st v,v1 // u2,v2 & v,v1 '//' w,w1 & v <> v1 holds
u2,v2 '//' w,w1 )
proof
let AS be Oriented_Orthogonality_Space; ::_thesis: ( AS is left_transitive iff for v, v1, w, w1, u2, v2 being Element of AS st v,v1 // u2,v2 & v,v1 '//' w,w1 & v <> v1 holds
u2,v2 '//' w,w1 )
A1: ( ( for v, v1, w, w1, u2, v2 being Element of AS st v,v1 // u2,v2 & v,v1 '//' w,w1 & v <> v1 holds
u2,v2 '//' w,w1 ) implies for u, u1, u2, v, v1, v2, w, w1 being Element of AS st u,u1 '//' v,v1 & v,v1 '//' w,w1 & u,u1 '//' u2,v2 & not u = u1 & not v = v1 holds
u2,v2 '//' w,w1 )
proof
assume A2: for v, v1, w, w1, u2, v2 being Element of AS st v,v1 // u2,v2 & v,v1 '//' w,w1 & v <> v1 holds
u2,v2 '//' w,w1 ; ::_thesis: for u, u1, u2, v, v1, v2, w, w1 being Element of AS st u,u1 '//' v,v1 & v,v1 '//' w,w1 & u,u1 '//' u2,v2 & not u = u1 & not v = v1 holds
u2,v2 '//' w,w1
let u, u1, u2, v, v1, v2, w, w1 be Element of AS; ::_thesis: ( u,u1 '//' v,v1 & v,v1 '//' w,w1 & u,u1 '//' u2,v2 & not u = u1 & not v = v1 implies u2,v2 '//' w,w1 )
assume that
A3: u,u1 '//' v,v1 and
A4: v,v1 '//' w,w1 and
A5: u,u1 '//' u2,v2 ; ::_thesis: ( u = u1 or v = v1 or u2,v2 '//' w,w1 )
now__::_thesis:_(_u_<>_u1_&_v_<>_v1_&_not_u_=_u1_&_not_v_=_v1_implies_u2,v2_'//'_w,w1_)
assume that
A6: u <> u1 and
 v <> v1 ; ::_thesis: ( u = u1 or v = v1 or u2,v2 '//' w,w1 )
 v,v1 // u2,v2 by A3, A5, A6, Def3;
hence  ( u = u1 or v = v1 or u2,v2 '//' w,w1 ) by A2, A4; ::_thesis: verum
end;
hence  ( u = u1 or v = v1 or u2,v2 '//' w,w1 ) ; ::_thesis: verum
end;
 ( AS is left_transitive implies for v, v1, w, w1, u2, v2 being Element of AS st v,v1 // u2,v2 & v,v1 '//' w,w1 & v <> v1 holds
u2,v2 '//' w,w1 )
proof
assume A7: AS is left_transitive ; ::_thesis: for v, v1, w, w1, u2, v2 being Element of AS st v,v1 // u2,v2 & v,v1 '//' w,w1 & v <> v1 holds
u2,v2 '//' w,w1
let v, v1, w, w1, u2, v2 be Element of AS; ::_thesis: ( v,v1 // u2,v2 & v,v1 '//' w,w1 & v <> v1 implies u2,v2 '//' w,w1 )
assume that
A8: v,v1 // u2,v2 and
A9: v,v1 '//' w,w1 and
A10: v <> v1 ; ::_thesis: u2,v2 '//' w,w1
 ex u, u1 being Element of AS st
( u <> u1 & u,u1 '//' v,v1 & u,u1 '//' u2,v2 ) by A8, Def3;
hence  u2,v2 '//' w,w1 by A7, A9, A10, Def6; ::_thesis: verum
end;
hence  ( AS is left_transitive iff for v, v1, w, w1, u2, v2 being Element of AS st v,v1 // u2,v2 & v,v1 '//' w,w1 & v <> v1 holds
u2,v2 '//' w,w1 ) by A1, Def6; ::_thesis: verum
end;

theorem Th11: :: DIRORT:11
for AS being Oriented_Orthogonality_Space holds
( AS is bach_transitive iff for u, u1, u2, v, v1, v2 being Element of AS st u,u1 '//' v,v1 & v,v1 // u2,v2 & v <> v1 holds
u,u1 '//' u2,v2 )
proof
let AS be Oriented_Orthogonality_Space; ::_thesis: ( AS is bach_transitive iff for u, u1, u2, v, v1, v2 being Element of AS st u,u1 '//' v,v1 & v,v1 // u2,v2 & v <> v1 holds
u,u1 '//' u2,v2 )
A1: ( ( for u, u1, u2, v, v1, v2 being Element of AS st u,u1 '//' v,v1 & v,v1 // u2,v2 & v <> v1 holds
u,u1 '//' u2,v2 ) implies for u, u1, u2, v, v1, v2, w, w1 being Element of AS st u,u1 '//' v,v1 & w,w1 '//' v,v1 & w,w1 '//' u2,v2 & not w = w1 & not v = v1 holds
u,u1 '//' u2,v2 )
proof
assume A2: for u, u1, u2, v, v1, v2 being Element of AS st u,u1 '//' v,v1 & v,v1 // u2,v2 & v <> v1 holds
u,u1 '//' u2,v2 ; ::_thesis: for u, u1, u2, v, v1, v2, w, w1 being Element of AS st u,u1 '//' v,v1 & w,w1 '//' v,v1 & w,w1 '//' u2,v2 & not w = w1 & not v = v1 holds
u,u1 '//' u2,v2
let u, u1, u2, v, v1, v2, w, w1 be Element of AS; ::_thesis: ( u,u1 '//' v,v1 & w,w1 '//' v,v1 & w,w1 '//' u2,v2 & not w = w1 & not v = v1 implies u,u1 '//' u2,v2 )
assume that
A3: u,u1 '//' v,v1 and
A4: w,w1 '//' v,v1 and
A5: w,w1 '//' u2,v2 ; ::_thesis: ( w = w1 or v = v1 or u,u1 '//' u2,v2 )
now__::_thesis:_(_w_<>_w1_&_v_<>_v1_&_not_w_=_w1_&_not_v_=_v1_implies_u,u1_'//'_u2,v2_)
assume that
A6: w <> w1 and
 v <> v1 ; ::_thesis: ( w = w1 or v = v1 or u,u1 '//' u2,v2 )
 v,v1 // u2,v2 by A4, A5, A6, Def3;
hence  ( w = w1 or v = v1 or u,u1 '//' u2,v2 ) by A2, A3; ::_thesis: verum
end;
hence  ( w = w1 or v = v1 or u,u1 '//' u2,v2 ) ; ::_thesis: verum
end;
 ( AS is bach_transitive implies for u, u1, u2, v, v1, v2 being Element of AS st u,u1 '//' v,v1 & v,v1 // u2,v2 & v <> v1 holds
u,u1 '//' u2,v2 )
proof
assume A7: AS is bach_transitive ; ::_thesis: for u, u1, u2, v, v1, v2 being Element of AS st u,u1 '//' v,v1 & v,v1 // u2,v2 & v <> v1 holds
u,u1 '//' u2,v2
let u, u1, u2, v, v1, v2 be Element of AS; ::_thesis: ( u,u1 '//' v,v1 & v,v1 // u2,v2 & v <> v1 implies u,u1 '//' u2,v2 )
assume that
A8: u,u1 '//' v,v1 and
A9: v,v1 // u2,v2 and
A10: v <> v1 ; ::_thesis: u,u1 '//' u2,v2
 ex w, w1 being Element of AS st
( w <> w1 & w,w1 '//' v,v1 & w,w1 '//' u2,v2 ) by A9, Def3;
hence  u,u1 '//' u2,v2 by A7, A8, A10, Def4; ::_thesis: verum
end;
hence  ( AS is bach_transitive iff for u, u1, u2, v, v1, v2 being Element of AS st u,u1 '//' v,v1 & v,v1 // u2,v2 & v <> v1 holds
u,u1 '//' u2,v2 ) by A1, Def4; ::_thesis: verum
end;

theorem :: DIRORT:12
for AS being Oriented_Orthogonality_Space st AS is bach_transitive holds
for u, u1, v, v1, w, w1 being Element of AS st u,u1 // v,v1 & v,v1 // w,w1 & v <> v1 holds
u,u1 // w,w1
proof
let AS be Oriented_Orthogonality_Space; ::_thesis: ( AS is bach_transitive implies for u, u1, v, v1, w, w1 being Element of AS st u,u1 // v,v1 & v,v1 // w,w1 & v <> v1 holds
u,u1 // w,w1 )
assume A1: AS is bach_transitive ; ::_thesis: for u, u1, v, v1, w, w1 being Element of AS st u,u1 // v,v1 & v,v1 // w,w1 & v <> v1 holds
u,u1 // w,w1
let u, u1, v, v1, w, w1 be Element of AS; ::_thesis: ( u,u1 // v,v1 & v,v1 // w,w1 & v <> v1 implies u,u1 // w,w1 )
assume that
A2: u,u1 // v,v1 and
A3: v,v1 // w,w1 and
A4: v <> v1 ; ::_thesis: u,u1 // w,w1
consider v2, v3 being Element of AS such that
A5: v2 <> v3 and
A6: v2,v3 '//' u,u1 and
A7: v2,v3 '//' v,v1 by A2, Def3;
 v2,v3 '//' w,w1 by A1, A3, A4, A7, Th11;
hence  u,u1 // w,w1 by A5, A6, Def3; ::_thesis: verum
end;

theorem Th13: :: DIRORT:13
for V being RealLinearSpace
for x, y being VECTOR of V
for AS being Oriented_Orthogonality_Space st Gen x,y & AS = CESpace (V,x,y) holds
( AS is Euclidean_like & AS is left_transitive & AS is right_transitive & AS is bach_transitive )
proof
let V be RealLinearSpace; ::_thesis: for x, y being VECTOR of V
for AS being Oriented_Orthogonality_Space st Gen x,y & AS = CESpace (V,x,y) holds
( AS is Euclidean_like & AS is left_transitive & AS is right_transitive & AS is bach_transitive )
let x, y be VECTOR of V; ::_thesis: for AS being Oriented_Orthogonality_Space st Gen x,y & AS = CESpace (V,x,y) holds
( AS is Euclidean_like & AS is left_transitive & AS is right_transitive & AS is bach_transitive )
let AS be Oriented_Orthogonality_Space; ::_thesis: ( Gen x,y & AS = CESpace (V,x,y) implies ( AS is Euclidean_like & AS is left_transitive & AS is right_transitive & AS is bach_transitive ) )
assume that
A1: Gen x,y and
A2: AS = CESpace (V,x,y) ; ::_thesis: ( AS is Euclidean_like & AS is left_transitive & AS is right_transitive & AS is bach_transitive )
A3: CESpace (V,x,y) = AffinStruct(# the carrier of V,(CORTE (V,x,y)) #) by ANALORT:def_7;
A4: now__::_thesis:_for_u,_u1,_u2,_v,_v1,_v2,_w,_w1_being_Element_of_AS_st_u,u1_'//'_v,v1_&_v,v1_'//'_w,w1_&_u2,v2_'//'_w,w1_&_not_w_=_w1_&_not_v_=_v1_holds_
u,u1_'//'_u2,v2
let u, u1, u2, v, v1, v2, w, w1 be Element of AS; ::_thesis: ( u,u1 '//' v,v1 & v,v1 '//' w,w1 & u2,v2 '//' w,w1 & not w = w1 & not v = v1 implies u,u1 '//' u2,v2 )
thus  ( u,u1 '//' v,v1 & v,v1 '//' w,w1 & u2,v2 '//' w,w1 & not w = w1 & not v = v1 implies u,u1 '//' u2,v2 ) ::_thesis: verum
proof
reconsider u9 = u, v9 = v, w9 = w, u19 = u1, v19 = v1, w19 = w1, u29 = u2, v29 = v2 as Element of V by A2, A3;
 ( u9,u19,v9,v19 are_COrte_wrt x,y & v9,v19,w9,w19 are_COrte_wrt x,y & u29,v29,w9,w19 are_COrte_wrt x,y & not w9 = w19 & not v9 = v19 implies u9,u19,u29,v29 are_COrte_wrt x,y ) by A1, ANALORT:44;
hence  ( u,u1 '//' v,v1 & v,v1 '//' w,w1 & u2,v2 '//' w,w1 & not w = w1 & not v = v1 implies u,u1 '//' u2,v2 ) by A2, ANALORT:54; ::_thesis: verum
end;
end;
A5: now__::_thesis:_for_u,_u1,_v,_v1_being_Element_of_AS_st_u,u1_'//'_v,v1_holds_
v,v1_'//'_u1,u
let u, u1, v, v1 be Element of AS; ::_thesis: ( u,u1 '//' v,v1 implies v,v1 '//' u1,u )
thus  ( u,u1 '//' v,v1 implies v,v1 '//' u1,u ) ::_thesis: verum
proof
reconsider u9 = u, v9 = v, u19 = u1, v19 = v1 as Element of V by A2, A3;
 ( u9,u19,v9,v19 are_COrte_wrt x,y implies v9,v19,u19,u9 are_COrte_wrt x,y ) by A1, ANALORT:18;
hence  ( u,u1 '//' v,v1 implies v,v1 '//' u1,u ) by A2, ANALORT:54; ::_thesis: verum
end;
end;
A6: now__::_thesis:_for_u,_u1,_u2,_v,_v1,_v2,_w,_w1_being_Element_of_AS_st_u,u1_'//'_v,v1_&_v,v1_'//'_w,w1_&_u,u1_'//'_u2,v2_&_not_u_=_u1_&_not_v_=_v1_holds_
u2,v2_'//'_w,w1
let u, u1, u2, v, v1, v2, w, w1 be Element of AS; ::_thesis: ( u,u1 '//' v,v1 & v,v1 '//' w,w1 & u,u1 '//' u2,v2 & not u = u1 & not v = v1 implies u2,v2 '//' w,w1 )
thus  ( u,u1 '//' v,v1 & v,v1 '//' w,w1 & u,u1 '//' u2,v2 & not u = u1 & not v = v1 implies u2,v2 '//' w,w1 ) ::_thesis: verum
proof
reconsider u9 = u, v9 = v, w9 = w, u19 = u1, v19 = v1, w19 = w1, u29 = u2, v29 = v2 as Element of V by A2, A3;
 ( u9,u19,v9,v19 are_COrte_wrt x,y & v9,v19,w9,w19 are_COrte_wrt x,y & u9,u19,u29,v29 are_COrte_wrt x,y & not u9 = u19 & not v9 = v19 implies u29,v29,w9,w19 are_COrte_wrt x,y ) by A1, ANALORT:46;
hence  ( u,u1 '//' v,v1 & v,v1 '//' w,w1 & u,u1 '//' u2,v2 & not u = u1 & not v = v1 implies u2,v2 '//' w,w1 ) by A2, ANALORT:54; ::_thesis: verum
end;
end;
now__::_thesis:_for_u,_u1,_u2,_v,_v1,_v2,_w,_w1_being_Element_of_AS_st_u,u1_'//'_v,v1_&_w,w1_'//'_v,v1_&_w,w1_'//'_u2,v2_&_not_w_=_w1_&_not_v_=_v1_holds_
u,u1_'//'_u2,v2
let u, u1, u2, v, v1, v2, w, w1 be Element of AS; ::_thesis: ( u,u1 '//' v,v1 & w,w1 '//' v,v1 & w,w1 '//' u2,v2 & not w = w1 & not v = v1 implies u,u1 '//' u2,v2 )
thus  ( u,u1 '//' v,v1 & w,w1 '//' v,v1 & w,w1 '//' u2,v2 & not w = w1 & not v = v1 implies u,u1 '//' u2,v2 ) ::_thesis: verum
proof
reconsider u9 = u, v9 = v, w9 = w, u19 = u1, v19 = v1, w19 = w1, u29 = u2, v29 = v2 as Element of V by A2, A3;
 ( u9,u19,v9,v19 are_COrte_wrt x,y & w9,w19,v9,v19 are_COrte_wrt x,y & w9,w19,u29,v29 are_COrte_wrt x,y & not w9 = w19 & not v9 = v19 implies u9,u19,u29,v29 are_COrte_wrt x,y ) by A1, ANALORT:42;
hence  ( u,u1 '//' v,v1 & w,w1 '//' v,v1 & w,w1 '//' u2,v2 & not w = w1 & not v = v1 implies u,u1 '//' u2,v2 ) by A2, ANALORT:54; ::_thesis: verum
end;
end;
hence  ( AS is Euclidean_like & AS is left_transitive & AS is right_transitive & AS is bach_transitive ) by A4, A6, A5, Def4, Def5, Def6, Def7; ::_thesis: verum
end;

registration
cluster non empty Oriented_Orthogonality_Space-like bach_transitive right_transitive left_transitive Euclidean_like for AffinStruct ;
existence
 ex b1 being Oriented_Orthogonality_Space st
( b1 is Euclidean_like & b1 is left_transitive & b1 is right_transitive & b1 is bach_transitive )
proof
consider V being RealLinearSpace, x, y being VECTOR of V such that
A1: Gen x,y by ANALMETR:3;
reconsider AS = CESpace (V,x,y) as Oriented_Orthogonality_Space by A1, Th4;
take  AS ; ::_thesis: ( AS is Euclidean_like & AS is left_transitive & AS is right_transitive & AS is bach_transitive )
thus  ( AS is Euclidean_like & AS is left_transitive & AS is right_transitive & AS is bach_transitive ) by A1, Th13; ::_thesis: verum
end;
end;

theorem Th14: :: DIRORT:14
for V being RealLinearSpace
for x, y being VECTOR of V
for AS being Oriented_Orthogonality_Space st Gen x,y & AS = CMSpace (V,x,y) holds
( AS is Minkowskian_like & AS is left_transitive & AS is right_transitive & AS is bach_transitive )
proof
let V be RealLinearSpace; ::_thesis: for x, y being VECTOR of V
for AS being Oriented_Orthogonality_Space st Gen x,y & AS = CMSpace (V,x,y) holds
( AS is Minkowskian_like & AS is left_transitive & AS is right_transitive & AS is bach_transitive )
let x, y be VECTOR of V; ::_thesis: for AS being Oriented_Orthogonality_Space st Gen x,y & AS = CMSpace (V,x,y) holds
( AS is Minkowskian_like & AS is left_transitive & AS is right_transitive & AS is bach_transitive )
let AS be Oriented_Orthogonality_Space; ::_thesis: ( Gen x,y & AS = CMSpace (V,x,y) implies ( AS is Minkowskian_like & AS is left_transitive & AS is right_transitive & AS is bach_transitive ) )
assume that
A1: Gen x,y and
A2: AS = CMSpace (V,x,y) ; ::_thesis: ( AS is Minkowskian_like & AS is left_transitive & AS is right_transitive & AS is bach_transitive )
A3: CMSpace (V,x,y) = AffinStruct(# the carrier of V,(CORTM (V,x,y)) #) by ANALORT:def_8;
A4: now__::_thesis:_for_u,_u1,_u2,_v,_v1,_v2,_w,_w1_being_Element_of_AS_st_u,u1_'//'_v,v1_&_v,v1_'//'_w,w1_&_u2,v2_'//'_w,w1_&_not_w_=_w1_&_not_v_=_v1_holds_
u,u1_'//'_u2,v2
let u, u1, u2, v, v1, v2, w, w1 be Element of AS; ::_thesis: ( u,u1 '//' v,v1 & v,v1 '//' w,w1 & u2,v2 '//' w,w1 & not w = w1 & not v = v1 implies u,u1 '//' u2,v2 )
thus  ( u,u1 '//' v,v1 & v,v1 '//' w,w1 & u2,v2 '//' w,w1 & not w = w1 & not v = v1 implies u,u1 '//' u2,v2 ) ::_thesis: verum
proof
reconsider u9 = u, v9 = v, w9 = w, u19 = u1, v19 = v1, w19 = w1, u29 = u2, v29 = v2 as Element of V by A2, A3;
 ( u9,u19,v9,v19 are_COrtm_wrt x,y & v9,v19,w9,w19 are_COrtm_wrt x,y & u29,v29,w9,w19 are_COrtm_wrt x,y & not w9 = w19 & not v9 = v19 implies u9,u19,u29,v29 are_COrtm_wrt x,y ) by A1, ANALORT:45;
hence  ( u,u1 '//' v,v1 & v,v1 '//' w,w1 & u2,v2 '//' w,w1 & not w = w1 & not v = v1 implies u,u1 '//' u2,v2 ) by A2, ANALORT:55; ::_thesis: verum
end;
end;
A5: now__::_thesis:_for_u,_u1,_v,_v1_being_Element_of_AS_st_u,u1_'//'_v,v1_holds_
v,v1_'//'_u,u1
let u, u1, v, v1 be Element of AS; ::_thesis: ( u,u1 '//' v,v1 implies v,v1 '//' u,u1 )
thus  ( u,u1 '//' v,v1 implies v,v1 '//' u,u1 ) ::_thesis: verum
proof
reconsider u9 = u, v9 = v, u19 = u1, v19 = v1 as Element of V by A2, A3;
 ( u9,u19,v9,v19 are_COrtm_wrt x,y implies v9,v19,u9,u19 are_COrtm_wrt x,y ) by A1, ANALORT:19;
hence  ( u,u1 '//' v,v1 implies v,v1 '//' u,u1 ) by A2, ANALORT:55; ::_thesis: verum
end;
end;
A6: now__::_thesis:_for_u,_u1,_u2,_v,_v1,_v2,_w,_w1_being_Element_of_AS_st_u,u1_'//'_v,v1_&_v,v1_'//'_w,w1_&_u,u1_'//'_u2,v2_&_not_u_=_u1_&_not_v_=_v1_holds_
u2,v2_'//'_w,w1
let u, u1, u2, v, v1, v2, w, w1 be Element of AS; ::_thesis: ( u,u1 '//' v,v1 & v,v1 '//' w,w1 & u,u1 '//' u2,v2 & not u = u1 & not v = v1 implies u2,v2 '//' w,w1 )
thus  ( u,u1 '//' v,v1 & v,v1 '//' w,w1 & u,u1 '//' u2,v2 & not u = u1 & not v = v1 implies u2,v2 '//' w,w1 ) ::_thesis: verum
proof
reconsider u9 = u, v9 = v, w9 = w, u19 = u1, v19 = v1, w19 = w1, u29 = u2, v29 = v2 as Element of V by A2, A3;
 ( u9,u19,v9,v19 are_COrtm_wrt x,y & v9,v19,w9,w19 are_COrtm_wrt x,y & u9,u19,u29,v29 are_COrtm_wrt x,y & not u9 = u19 & not v9 = v19 implies u29,v29,w9,w19 are_COrtm_wrt x,y ) by A1, ANALORT:47;
hence  ( u,u1 '//' v,v1 & v,v1 '//' w,w1 & u,u1 '//' u2,v2 & not u = u1 & not v = v1 implies u2,v2 '//' w,w1 ) by A2, ANALORT:55; ::_thesis: verum
end;
end;
now__::_thesis:_for_u,_u1,_u2,_v,_v1,_v2,_w,_w1_being_Element_of_AS_st_u,u1_'//'_v,v1_&_w,w1_'//'_v,v1_&_w,w1_'//'_u2,v2_&_not_w_=_w1_&_not_v_=_v1_holds_
u,u1_'//'_u2,v2
let u, u1, u2, v, v1, v2, w, w1 be Element of AS; ::_thesis: ( u,u1 '//' v,v1 & w,w1 '//' v,v1 & w,w1 '//' u2,v2 & not w = w1 & not v = v1 implies u,u1 '//' u2,v2 )
thus  ( u,u1 '//' v,v1 & w,w1 '//' v,v1 & w,w1 '//' u2,v2 & not w = w1 & not v = v1 implies u,u1 '//' u2,v2 ) ::_thesis: verum
proof
reconsider u9 = u, v9 = v, w9 = w, u19 = u1, v19 = v1, w19 = w1, u29 = u2, v29 = v2 as Element of V by A2, A3;
 ( u9,u19,v9,v19 are_COrtm_wrt x,y & w9,w19,v9,v19 are_COrtm_wrt x,y & w9,w19,u29,v29 are_COrtm_wrt x,y & not w9 = w19 & not v9 = v19 implies u9,u19,u29,v29 are_COrtm_wrt x,y ) by A1, ANALORT:43;
hence  ( u,u1 '//' v,v1 & w,w1 '//' v,v1 & w,w1 '//' u2,v2 & not w = w1 & not v = v1 implies u,u1 '//' u2,v2 ) by A2, ANALORT:55; ::_thesis: verum
end;
end;
hence  ( AS is Minkowskian_like & AS is left_transitive & AS is right_transitive & AS is bach_transitive ) by A4, A6, A5, Def4, Def5, Def6, Def8; ::_thesis: verum
end;

registration
cluster non empty Oriented_Orthogonality_Space-like bach_transitive right_transitive left_transitive Minkowskian_like for AffinStruct ;
existence
 ex b1 being Oriented_Orthogonality_Space st
( b1 is Minkowskian_like & b1 is left_transitive & b1 is right_transitive & b1 is bach_transitive )
proof
consider V being RealLinearSpace, x, y being VECTOR of V such that
A1: Gen x,y by ANALMETR:3;
reconsider AS = CMSpace (V,x,y) as Oriented_Orthogonality_Space by A1, Th3;
take  AS ; ::_thesis: ( AS is Minkowskian_like & AS is left_transitive & AS is right_transitive & AS is bach_transitive )
thus  ( AS is Minkowskian_like & AS is left_transitive & AS is right_transitive & AS is bach_transitive ) by A1, Th14; ::_thesis: verum
end;
end;

theorem Th15: :: DIRORT:15
for AS being Oriented_Orthogonality_Space st AS is left_transitive holds
AS is right_transitive
proof
let AS be Oriented_Orthogonality_Space; ::_thesis: ( AS is left_transitive implies AS is right_transitive )
 ( ( for u, u1, u2, v, v1, v2, w, w1 being Element of AS st u,u1 '//' v,v1 & v,v1 '//' w,w1 & u,u1 '//' u2,v2 & not u = u1 & not v = v1 holds
u2,v2 '//' w,w1 ) implies for u, u1, u2, v, v1, v2, w, w1 being Element of AS st u,u1 '//' v,v1 & v,v1 '//' w,w1 & u2,v2 '//' w,w1 & not w = w1 & not v = v1 holds
u,u1 '//' u2,v2 )
proof
assume A1: for u, u1, u2, v, v1, v2, w, w1 being Element of AS st u,u1 '//' v,v1 & v,v1 '//' w,w1 & u,u1 '//' u2,v2 & not u = u1 & not v = v1 holds
u2,v2 '//' w,w1 ; ::_thesis: for u, u1, u2, v, v1, v2, w, w1 being Element of AS st u,u1 '//' v,v1 & v,v1 '//' w,w1 & u2,v2 '//' w,w1 & not w = w1 & not v = v1 holds
u,u1 '//' u2,v2
let u, u1, u2, v, v1, v2, w, w1 be Element of AS; ::_thesis: ( u,u1 '//' v,v1 & v,v1 '//' w,w1 & u2,v2 '//' w,w1 & not w = w1 & not v = v1 implies u,u1 '//' u2,v2 )
assume that
A2: u,u1 '//' v,v1 and
A3: v,v1 '//' w,w1 and
A4: u2,v2 '//' w,w1 ; ::_thesis: ( w = w1 or v = v1 or u,u1 '//' u2,v2 )
A5: ( ( not w = w1 & not v = v1 & not u,u1 '//' u2,v2 & not u,u1 '//' v2,u2 ) or w = w1 or v = v1 or u,u1 '//' u2,v2 )
proof
now__::_thesis:_(_(_not_w_=_w1_&_not_v_=_v1_&_not_u,u1_'//'_u2,v2_&_not_u,u1_'//'_v2,u2_)_or_w_=_w1_or_v_=_v1_or_u,u1_'//'_u2,v2_)
A6: now__::_thesis:_(_not_v2,u2_'//'_w,w1_or_(_not_w_=_w1_&_not_v_=_v1_&_not_u,u1_'//'_u2,v2_&_not_u,u1_'//'_v2,u2_)_or_w_=_w1_or_v_=_v1_or_u,u1_'//'_u2,v2_)
assume  v2,u2 '//' w,w1 ; ::_thesis: ( ( not w = w1 & not v = v1 & not u,u1 '//' u2,v2 & not u,u1 '//' v2,u2 ) or w = w1 or v = v1 or u,u1 '//' u2,v2 )
then  u2,v2 '//' w1,w by Def1;
then  ( u2 = v2 or w = w1 ) by A4, Def1;
hence  ( ( not w = w1 & not v = v1 & not u,u1 '//' u2,v2 & not u,u1 '//' v2,u2 ) or w = w1 or v = v1 or u,u1 '//' u2,v2 ) ; ::_thesis: verum
end;
 ( not u = u1 or ( not w = w1 & not v = v1 & not u,u1 '//' u2,v2 & not u,u1 '//' v2,u2 ) or w = w1 or v = v1 or u,u1 '//' u2,v2 ) by Def1;
hence  ( ( not w = w1 & not v = v1 & not u,u1 '//' u2,v2 & not u,u1 '//' v2,u2 ) or w = w1 or v = v1 or u,u1 '//' u2,v2 ) by A1, A2, A3, A6; ::_thesis: verum
end;
hence  ( ( not w = w1 & not v = v1 & not u,u1 '//' u2,v2 & not u,u1 '//' v2,u2 ) or w = w1 or v = v1 or u,u1 '//' u2,v2 ) ; ::_thesis: verum
end;
A7: now__::_thesis:_(_w,w1_'//'_v,v1_&_v,v1_'//'_u,u1_&_w,w1_'//'_v2,u2_&_not_w_=_w1_&_not_v_=_v1_implies_u,u1_'//'_u2,v2_)
assume that
A8: w,w1 '//' v,v1 and
A9: v,v1 '//' u,u1 and
A10: w,w1 '//' v2,u2 ; ::_thesis: ( w = w1 or v = v1 or u,u1 '//' u2,v2 )
 ( w = w1 or v = v1 or v2,u2 '//' u,u1 ) by A1, A8, A9, A10;
hence  ( w = w1 or v = v1 or u,u1 '//' u2,v2 ) by A5, Def1; ::_thesis: verum
end;
A11: now__::_thesis:_(_w,w1_'//'_v1,v_&_v,v1_'//'_u,u1_&_w,w1_'//'_v2,u2_&_not_w_=_w1_&_not_v_=_v1_implies_u,u1_'//'_u2,v2_)
assume that
A12: w,w1 '//' v1,v and
A13: v,v1 '//' u,u1 and
A14: w,w1 '//' v2,u2 ; ::_thesis: ( w = w1 or v = v1 or u,u1 '//' u2,v2 )
 v1,v '//' u1,u by A13, Def1;
then  ( w = w1 or v = v1 or v2,u2 '//' u1,u ) by A1, A12, A14;
then  ( w = w1 or v = v1 or u2,v2 '//' u,u1 ) by Def1;
hence  ( w = w1 or v = v1 or u,u1 '//' u2,v2 ) by A5, Def1; ::_thesis: verum
end;
A15: now__::_thesis:_(_w,w1_'//'_v1,v_&_v,v1_'//'_u,u1_&_w,w1_'//'_u2,v2_&_not_w_=_w1_&_not_v_=_v1_implies_u,u1_'//'_u2,v2_)
assume that
A16: w,w1 '//' v1,v and
A17: v,v1 '//' u,u1 and
A18: w,w1 '//' u2,v2 ; ::_thesis: ( w = w1 or v = v1 or u,u1 '//' u2,v2 )
 v1,v '//' u1,u by A17, Def1;
then  ( w = w1 or v = v1 or u2,v2 '//' u1,u ) by A1, A16, A18;
then  ( w = w1 or v = v1 or v2,u2 '//' u,u1 ) by Def1;
hence  ( w = w1 or v = v1 or u,u1 '//' u2,v2 ) by A5, Def1; ::_thesis: verum
end;
A19: now__::_thesis:_(_w,w1_'//'_v1,v_&_v,v1_'//'_u1,u_&_w,w1_'//'_v2,u2_&_not_w_=_w1_&_not_v_=_v1_implies_u,u1_'//'_u2,v2_)
assume that
A20: w,w1 '//' v1,v and
A21: v,v1 '//' u1,u and
A22: w,w1 '//' v2,u2 ; ::_thesis: ( w = w1 or v = v1 or u,u1 '//' u2,v2 )
 v1,v '//' u,u1 by A21, Def1;
then  ( w = w1 or v = v1 or v2,u2 '//' u,u1 ) by A1, A20, A22;
hence  ( w = w1 or v = v1 or u,u1 '//' u2,v2 ) by A5, Def1; ::_thesis: verum
end;
A23: now__::_thesis:_(_w,w1_'//'_v1,v_&_v,v1_'//'_u1,u_&_w,w1_'//'_u2,v2_&_not_w_=_w1_&_not_v_=_v1_implies_u,u1_'//'_u2,v2_)
assume that
A24: w,w1 '//' v1,v and
A25: v,v1 '//' u1,u and
A26: w,w1 '//' u2,v2 ; ::_thesis: ( w = w1 or v = v1 or u,u1 '//' u2,v2 )
 v1,v '//' u,u1 by A25, Def1;
then  ( w = w1 or v1 = v or u2,v2 '//' u,u1 ) by A1, A24, A26;
hence  ( w = w1 or v = v1 or u,u1 '//' u2,v2 ) by A5, Def1; ::_thesis: verum
end;
A27: now__::_thesis:_(_w,w1_'//'_v,v1_&_v,v1_'//'_u1,u_&_w,w1_'//'_v2,u2_&_not_w_=_w1_&_not_v_=_v1_implies_u,u1_'//'_u2,v2_)
assume that
A28: w,w1 '//' v,v1 and
A29: v,v1 '//' u1,u and
A30: w,w1 '//' v2,u2 ; ::_thesis: ( w = w1 or v = v1 or u,u1 '//' u2,v2 )
 ( w = w1 or v = v1 or v2,u2 '//' u1,u ) by A1, A28, A29, A30;
then  ( w = w1 or v = v1 or u1,u '//' u2,v2 or u1,u '//' v2,u2 ) by Def1;
hence  ( w = w1 or v = v1 or u,u1 '//' u2,v2 ) by A5, Def1; ::_thesis: verum
end;
A31: now__::_thesis:_(_w,w1_'//'_v,v1_&_v,v1_'//'_u1,u_&_w,w1_'//'_u2,v2_&_not_w_=_w1_&_not_v_=_v1_implies_u,u1_'//'_u2,v2_)
assume that
A32: w,w1 '//' v,v1 and
A33: v,v1 '//' u1,u and
A34: w,w1 '//' u2,v2 ; ::_thesis: ( w = w1 or v = v1 or u,u1 '//' u2,v2 )
 ( w = w1 or v = v1 or u2,v2 '//' u1,u ) by A1, A32, A33, A34;
then  ( w = w1 or v = v1 or u1,u '//' u2,v2 or u1,u '//' v2,u2 ) by Def1;
hence  ( w = w1 or v = v1 or u,u1 '//' u2,v2 ) by A5, Def1; ::_thesis: verum
end;
now__::_thesis:_(_w,w1_'//'_v,v1_&_v,v1_'//'_u,u1_&_w,w1_'//'_u2,v2_&_not_w_=_w1_&_not_v_=_v1_implies_u,u1_'//'_u2,v2_)
assume that
A35: w,w1 '//' v,v1 and
A36: v,v1 '//' u,u1 and
A37: w,w1 '//' u2,v2 ; ::_thesis: ( w = w1 or v = v1 or u,u1 '//' u2,v2 )
 ( w = w1 or v = v1 or u2,v2 '//' u,u1 ) by A1, A35, A36, A37;
hence  ( w = w1 or v = v1 or u,u1 '//' u2,v2 ) by A5, Def1; ::_thesis: verum
end;
hence  ( w = w1 or v = v1 or u,u1 '//' u2,v2 ) by A2, A3, A4, A7, A31, A27, A15, A11, A23, A19, Def1; ::_thesis: verum
end;
hence  ( AS is left_transitive implies AS is right_transitive ) by Def5, Def6; ::_thesis: verum
end;

theorem :: DIRORT:16
for AS being Oriented_Orthogonality_Space st AS is left_transitive holds
AS is bach_transitive
proof
let AS be Oriented_Orthogonality_Space; ::_thesis: ( AS is left_transitive implies AS is bach_transitive )
 ( ( for u, u1, u2, v, v1, v2, w, w1 being Element of AS st u,u1 '//' v,v1 & v,v1 '//' w,w1 & u,u1 '//' u2,v2 & not u = u1 & not v = v1 holds
u2,v2 '//' w,w1 ) implies for u, u1, u2, v, v1, v2, w, w1 being Element of AS st u,u1 '//' v,v1 & w,w1 '//' v,v1 & w,w1 '//' u2,v2 & not w = w1 & not v = v1 holds
u,u1 '//' u2,v2 )
proof
assume A1: for u, u1, u2, v, v1, v2, w, w1 being Element of AS st u,u1 '//' v,v1 & v,v1 '//' w,w1 & u,u1 '//' u2,v2 & not u = u1 & not v = v1 holds
u2,v2 '//' w,w1 ; ::_thesis: for u, u1, u2, v, v1, v2, w, w1 being Element of AS st u,u1 '//' v,v1 & w,w1 '//' v,v1 & w,w1 '//' u2,v2 & not w = w1 & not v = v1 holds
u,u1 '//' u2,v2
let u, u1, u2, v, v1, v2, w, w1 be Element of AS; ::_thesis: ( u,u1 '//' v,v1 & w,w1 '//' v,v1 & w,w1 '//' u2,v2 & not w = w1 & not v = v1 implies u,u1 '//' u2,v2 )
A2: ( AS is left_transitive implies AS is right_transitive ) by Th15;
then A3: ( u,u1 '//' v,v1 & v,v1 '//' w1,w & u2,v2 '//' w1,w & u,u1 '//' v,v1 & w,w1 '//' v,v1 & w,w1 '//' u2,v2 & not w = w1 & not v = v1 implies u,u1 '//' u2,v2 ) by A1, Def5, Def6;
assume that
A4: u,u1 '//' v,v1 and
A5: w,w1 '//' v,v1 and
A6: w,w1 '//' u2,v2 ; ::_thesis: ( w = w1 or v = v1 or u,u1 '//' u2,v2 )
A7: ( ( not v = v1 & not w = w1 & not u,u1 '//' u2,v2 & not u,u1 '//' v2,u2 ) or w = w1 or v = v1 or u,u1 '//' u2,v2 )
proof
A8: now__::_thesis:_(_u,u1_'//'_v2,u2_&_u_<>_u1_&_v_<>_v1_&_w_<>_w1_&_(_v_=_v1_or_w_=_w1_or_u,u1_'//'_u2,v2_or_u,u1_'//'_v2,u2_)_&_not_w_=_w1_&_not_v_=_v1_implies_u,u1_'//'_u2,v2_)
assume that
A9: u,u1 '//' v2,u2 and
A10: u <> u1 and
A11: v <> v1 and
 w <> w1 ; ::_thesis: ( ( not v = v1 & not w = w1 & not u,u1 '//' u2,v2 & not u,u1 '//' v2,u2 ) or w = w1 or v = v1 or u,u1 '//' u2,v2 )
A12: now__::_thesis:_(_not_u2,v2_'//'_u,u1_or_(_not_v_=_v1_&_not_w_=_w1_&_not_u,u1_'//'_u2,v2_&_not_u,u1_'//'_v2,u2_)_or_w_=_w1_or_v_=_v1_or_u,u1_'//'_u2,v2_)
assume A13: u2,v2 '//' u,u1 ; ::_thesis: ( ( not v = v1 & not w = w1 & not u,u1 '//' u2,v2 & not u,u1 '//' v2,u2 ) or w = w1 or v = v1 or u,u1 '//' u2,v2 )
then A14: u2,v2 '//' w,w1 by A2, A1, A4, A5, A10, A11, Def5, Def6;
A15: now__::_thesis:_(_not_u2,v2_'//'_w1,w_or_(_not_v_=_v1_&_not_w_=_w1_&_not_u,u1_'//'_u2,v2_&_not_u,u1_'//'_v2,u2_)_or_w_=_w1_or_v_=_v1_or_u,u1_'//'_u2,v2_)
assume  u2,v2 '//' w1,w ; ::_thesis: ( ( not v = v1 & not w = w1 & not u,u1 '//' u2,v2 & not u,u1 '//' v2,u2 ) or w = w1 or v = v1 or u,u1 '//' u2,v2 )
then  ( w = w1 or u2 = v2 ) by A14, Def1;
hence  ( ( not v = v1 & not w = w1 & not u,u1 '//' u2,v2 & not u,u1 '//' v2,u2 ) or w = w1 or v = v1 or u,u1 '//' u2,v2 ) ; ::_thesis: verum
end;
 w1,w '//' v2,u2 by A6, Def1;
then  ( u2,v2 '//' w1,w or u2 = v2 ) by A2, A1, A9, A10, A13, Def5, Def6;
hence  ( ( not v = v1 & not w = w1 & not u,u1 '//' u2,v2 & not u,u1 '//' v2,u2 ) or w = w1 or v = v1 or u,u1 '//' u2,v2 ) by A15; ::_thesis: verum
end;
A16: now__::_thesis:_(_not_u2,v2_'//'_u1,u_or_(_not_v_=_v1_&_not_w_=_w1_&_not_u,u1_'//'_u2,v2_&_not_u,u1_'//'_v2,u2_)_or_w_=_w1_or_v_=_v1_or_u,u1_'//'_u2,v2_)
A17: w1,w '//' v1,v by A5, Def1;
assume A18: u2,v2 '//' u1,u ; ::_thesis: ( ( not v = v1 & not w = w1 & not u,u1 '//' u2,v2 & not u,u1 '//' v2,u2 ) or w = w1 or v = v1 or u,u1 '//' u2,v2 )
 u1,u '//' v1,v by A4, Def1;
then A19: u2,v2 '//' w1,w by A2, A1, A10, A11, A18, A17, Def5, Def6;
A20: now__::_thesis:_(_not_u2,v2_'//'_w,w1_or_(_not_v_=_v1_&_not_w_=_w1_&_not_u,u1_'//'_u2,v2_&_not_u,u1_'//'_v2,u2_)_or_w_=_w1_or_v_=_v1_or_u,u1_'//'_u2,v2_)
assume  u2,v2 '//' w,w1 ; ::_thesis: ( ( not v = v1 & not w = w1 & not u,u1 '//' u2,v2 & not u,u1 '//' v2,u2 ) or w = w1 or v = v1 or u,u1 '//' u2,v2 )
then  ( w = w1 or u2 = v2 ) by A19, Def1;
hence  ( ( not v = v1 & not w = w1 & not u,u1 '//' u2,v2 & not u,u1 '//' v2,u2 ) or w = w1 or v = v1 or u,u1 '//' u2,v2 ) ; ::_thesis: verum
end;
 u1,u '//' u2,v2 by A9, Def1;
then  ( u2,v2 '//' w,w1 or u2 = v2 ) by A2, A1, A6, A10, A18, Def5, Def6;
hence  ( ( not v = v1 & not w = w1 & not u,u1 '//' u2,v2 & not u,u1 '//' v2,u2 ) or w = w1 or v = v1 or u,u1 '//' u2,v2 ) by A20; ::_thesis: verum
end;
 ( v2,u2 '//' u,u1 or v2,u2 '//' u1,u ) by A9, Def1;
hence  ( ( not v = v1 & not w = w1 & not u,u1 '//' u2,v2 & not u,u1 '//' v2,u2 ) or w = w1 or v = v1 or u,u1 '//' u2,v2 ) by A16, A12, Def1; ::_thesis: verum
end;
assume  ( v = v1 or w = w1 or u,u1 '//' u2,v2 or u,u1 '//' v2,u2 ) ; ::_thesis: ( w = w1 or v = v1 or u,u1 '//' u2,v2 )
hence  ( w = w1 or v = v1 or u,u1 '//' u2,v2 ) by A8, Def1; ::_thesis: verum
end;
A21: now__::_thesis:_(_u,u1_'//'_v,v1_&_v,v1_'//'_w,w1_&_u2,v2_'//'_w1,w_&_not_w_=_w1_&_not_v_=_v1_implies_u,u1_'//'_u2,v2_)
assume that
A22: u,u1 '//' v,v1 and
A23: v,v1 '//' w,w1 and
A24: u2,v2 '//' w1,w ; ::_thesis: ( w = w1 or v = v1 or u,u1 '//' u2,v2 )
 v2,u2 '//' w,w1 by A24, Def1;
hence  ( w = w1 or v = v1 or u,u1 '//' u2,v2 ) by A2, A1, A7, A22, A23, Def5, Def6; ::_thesis: verum
end;
A25: now__::_thesis:_(_u,u1_'//'_v,v1_&_v,v1_'//'_w1,w_&_u2,v2_'//'_w,w1_&_not_w_=_w1_&_not_v_=_v1_implies_u,u1_'//'_u2,v2_)
assume that
A26: u,u1 '//' v,v1 and
A27: v,v1 '//' w1,w and
A28: u2,v2 '//' w,w1 ; ::_thesis: ( w = w1 or v = v1 or u,u1 '//' u2,v2 )
 v2,u2 '//' w1,w by A28, Def1;
hence  ( w = w1 or v = v1 or u,u1 '//' u2,v2 ) by A2, A1, A7, A26, A27, Def5, Def6; ::_thesis: verum
end;
 ( u,u1 '//' v,v1 & v,v1 '//' w,w1 & u2,v2 '//' w,w1 & not w = w1 & not v = v1 implies u,u1 '//' u2,v2 ) by A2, A1, Def5, Def6;
hence  ( w = w1 or v = v1 or u,u1 '//' u2,v2 ) by A4, A5, A6, A21, A3, A25, Def1; ::_thesis: verum
end;
hence  ( AS is left_transitive implies AS is bach_transitive ) by Def4, Def6; ::_thesis: verum
end;

theorem :: DIRORT:17
for AS being Oriented_Orthogonality_Space st AS is bach_transitive holds
( AS is right_transitive iff for u, u1, v, v1, u2, v2 being Element of AS st u,u1 '//' u2,v2 & v,v1 '//' u2,v2 & u2 <> v2 holds
u,u1 // v,v1 )
proof
let AS be Oriented_Orthogonality_Space; ::_thesis: ( AS is bach_transitive implies ( AS is right_transitive iff for u, u1, v, v1, u2, v2 being Element of AS st u,u1 '//' u2,v2 & v,v1 '//' u2,v2 & u2 <> v2 holds
u,u1 // v,v1 ) )
A1: ( ( for u, u1, u2, v, v1, v2, w, w1 being Element of AS st u,u1 '//' v,v1 & v,v1 '//' w,w1 & u2,v2 '//' w,w1 & not w = w1 & not v = v1 holds
u,u1 '//' u2,v2 ) implies for u, u1, v, v1, u2, v2 being Element of AS st u,u1 '//' u2,v2 & v,v1 '//' u2,v2 & u2 <> v2 holds
u,u1 // v,v1 )
proof
set w = the Element of AS;
assume A2: for u, u1, u2, v, v1, v2, w, w1 being Element of AS st u,u1 '//' v,v1 & v,v1 '//' w,w1 & u2,v2 '//' w,w1 & not w = w1 & not v = v1 holds
u,u1 '//' u2,v2 ; ::_thesis: for u, u1, v, v1, u2, v2 being Element of AS st u,u1 '//' u2,v2 & v,v1 '//' u2,v2 & u2 <> v2 holds
u,u1 // v,v1
let u, u1, v, v1, u2, v2 be Element of AS; ::_thesis: ( u,u1 '//' u2,v2 & v,v1 '//' u2,v2 & u2 <> v2 implies u,u1 // v,v1 )
assume that
A3: u,u1 '//' u2,v2 and
A4: v,v1 '//' u2,v2 and
A5: u2 <> v2 ; ::_thesis: u,u1 // v,v1
consider w1 being Element of AS such that
A6: the Element of AS <> w1 and
A7: the Element of AS,w1 '//' u,u1 by Def1;
A8: now__::_thesis:_(_u_=_u1_implies_u,u1_//_v,v1_)
set w = the Element of AS;
assume A9: u = u1 ; ::_thesis: u,u1 // v,v1
consider w1 being Element of AS such that
A10: the Element of AS <> w1 and
A11: the Element of AS,w1 '//' v,v1 by Def1;
 the Element of AS,w1 '//' u,u by Def1;
hence  u,u1 // v,v1 by A9, A10, A11, Def3; ::_thesis: verum
end;
now__::_thesis:_(_u_<>_u1_implies_u,u1_//_v,v1_)
assume  u <> u1 ; ::_thesis: u,u1 // v,v1
then  the Element of AS,w1 '//' v,v1 by A2, A3, A4, A5, A7;
hence  u,u1 // v,v1 by A6, A7, Def3; ::_thesis: verum
end;
hence  u,u1 // v,v1 by A8; ::_thesis: verum
end;
assume A12: AS is bach_transitive ; ::_thesis: ( AS is right_transitive iff for u, u1, v, v1, u2, v2 being Element of AS st u,u1 '//' u2,v2 & v,v1 '//' u2,v2 & u2 <> v2 holds
u,u1 // v,v1 )
 ( ( for u, u1, v, v1, u2, v2 being Element of AS st u,u1 '//' u2,v2 & v,v1 '//' u2,v2 & u2 <> v2 holds
u,u1 // v,v1 ) implies for u, u1, u2, v, v1, v2, w, w1 being Element of AS st u,u1 '//' v,v1 & v,v1 '//' w,w1 & u2,v2 '//' w,w1 & not w = w1 & not v = v1 holds
u,u1 '//' u2,v2 )
proof
assume A13: for u, u1, v, v1, u2, v2 being Element of AS st u,u1 '//' u2,v2 & v,v1 '//' u2,v2 & u2 <> v2 holds
u,u1 // v,v1 ; ::_thesis: for u, u1, u2, v, v1, v2, w, w1 being Element of AS st u,u1 '//' v,v1 & v,v1 '//' w,w1 & u2,v2 '//' w,w1 & not w = w1 & not v = v1 holds
u,u1 '//' u2,v2
let u, u1, u2, v, v1, v2, w, w1 be Element of AS; ::_thesis: ( u,u1 '//' v,v1 & v,v1 '//' w,w1 & u2,v2 '//' w,w1 & not w = w1 & not v = v1 implies u,u1 '//' u2,v2 )
assume that
A14: u,u1 '//' v,v1 and
A15: v,v1 '//' w,w1 and
A16: u2,v2 '//' w,w1 ; ::_thesis: ( w = w1 or v = v1 or u,u1 '//' u2,v2 )
now__::_thesis:_(_w_<>_w1_&_v_<>_v1_&_not_w_=_w1_&_not_v_=_v1_implies_u,u1_'//'_u2,v2_)
assume that
A17: w <> w1 and
 v <> v1 ; ::_thesis: ( w = w1 or v = v1 or u,u1 '//' u2,v2 )
 v,v1 // u2,v2 by A13, A15, A16, A17;
then  ex u3, v3 being Element of AS st
( u3 <> v3 & u3,v3 '//' v,v1 & u3,v3 '//' u2,v2 ) by Def3;
hence  ( w = w1 or v = v1 or u,u1 '//' u2,v2 ) by A12, A14, Def4; ::_thesis: verum
end;
hence  ( w = w1 or v = v1 or u,u1 '//' u2,v2 ) ; ::_thesis: verum
end;
hence  ( AS is right_transitive iff for u, u1, v, v1, u2, v2 being Element of AS st u,u1 '//' u2,v2 & v,v1 '//' u2,v2 & u2 <> v2 holds
u,u1 // v,v1 ) by A1, Def5; ::_thesis: verum
end;

theorem :: DIRORT:18
for AS being Oriented_Orthogonality_Space st AS is right_transitive & ( AS is Euclidean_like or AS is Minkowskian_like ) holds
AS is left_transitive
proof
let AS be Oriented_Orthogonality_Space; ::_thesis: ( AS is right_transitive & ( AS is Euclidean_like or AS is Minkowskian_like ) implies AS is left_transitive )
assume A1: AS is right_transitive ; ::_thesis: ( ( not AS is Euclidean_like & not AS is Minkowskian_like ) or AS is left_transitive )
 ( ( for u, u1, v, v1 being Element of AS holds
not ( u,u1 '//' v,v1 & not v,v1 '//' u,u1 & ex u, u1, v, v1 being Element of AS st
( u,u1 '//' v,v1 & not v,v1 '//' u1,u ) ) ) implies for u, u1, u2, v, v1, v2, w, w1 being Element of AS st u,u1 '//' v,v1 & v,v1 '//' w,w1 & u,u1 '//' u2,v2 & not u = u1 & not v = v1 holds
u2,v2 '//' w,w1 )
proof
assume A2: for u, u1, v, v1 being Element of AS holds
not ( u,u1 '//' v,v1 & not v,v1 '//' u,u1 & ex u, u1, v, v1 being Element of AS st
( u,u1 '//' v,v1 & not v,v1 '//' u1,u ) ) ; ::_thesis: for u, u1, u2, v, v1, v2, w, w1 being Element of AS st u,u1 '//' v,v1 & v,v1 '//' w,w1 & u,u1 '//' u2,v2 & not u = u1 & not v = v1 holds
u2,v2 '//' w,w1
let u, u1, u2, v, v1, v2, w, w1 be Element of AS; ::_thesis: ( u,u1 '//' v,v1 & v,v1 '//' w,w1 & u,u1 '//' u2,v2 & not u = u1 & not v = v1 implies u2,v2 '//' w,w1 )
assume that
A3: u,u1 '//' v,v1 and
A4: v,v1 '//' w,w1 and
A5: u,u1 '//' u2,v2 ; ::_thesis: ( u = u1 or v = v1 or u2,v2 '//' w,w1 )
A6: now__::_thesis:_(_(_for_u,_u1,_v,_v1_being_Element_of_AS_st_u,u1_'//'_v,v1_holds_
v,v1_'//'_u1,u_)_&_not_u_=_u1_&_not_v_=_v1_implies_u2,v2_'//'_w,w1_)
assume A7: for u, u1, v, v1 being Element of AS st u,u1 '//' v,v1 holds
v,v1 '//' u1,u ; ::_thesis: ( u = u1 or v = v1 or u2,v2 '//' w,w1 )
now__::_thesis:_(_u_<>_u1_&_v_<>_v1_&_not_u_=_u1_&_not_v_=_v1_implies_u2,v2_'//'_w,w1_)
 w,w1 '//' v1,v by A4, A7;
then A8: w1,w '//' v,v1 by Def1;
A9: u2,v2 '//' u1,u by A5, A7;
assume that
A10: u <> u1 and
A11: v <> v1 ; ::_thesis: ( u = u1 or v = v1 or u2,v2 '//' w,w1 )
 v,v1 '//' u1,u by A3, A7;
then  w1,w '//' u2,v2 by A1, A10, A11, A8, A9, Def5;
hence  ( u = u1 or v = v1 or u2,v2 '//' w,w1 ) by A7; ::_thesis: verum
end;
hence  ( u = u1 or v = v1 or u2,v2 '//' w,w1 ) ; ::_thesis: verum
end;
now__::_thesis:_(_(_for_u,_u1,_v,_v1_being_Element_of_AS_st_u,u1_'//'_v,v1_holds_
v,v1_'//'_u,u1_)_&_not_u_=_u1_&_not_v_=_v1_implies_u2,v2_'//'_w,w1_)
assume A12: for u, u1, v, v1 being Element of AS st u,u1 '//' v,v1 holds
v,v1 '//' u,u1 ; ::_thesis: ( u = u1 or v = v1 or u2,v2 '//' w,w1 )
now__::_thesis:_(_u_<>_u1_&_v_<>_v1_&_not_u_=_u1_&_not_v_=_v1_implies_u2,v2_'//'_w,w1_)
A13: u2,v2 '//' u,u1 by A5, A12;
A14: w,w1 '//' v,v1 by A4, A12;
assume that
A15: u <> u1 and
A16: v <> v1 ; ::_thesis: ( u = u1 or v = v1 or u2,v2 '//' w,w1 )
 v,v1 '//' u,u1 by A3, A12;
then  w,w1 '//' u2,v2 by A1, A15, A16, A14, A13, Def5;
hence  ( u = u1 or v = v1 or u2,v2 '//' w,w1 ) by A12; ::_thesis: verum
end;
hence  ( u = u1 or v = v1 or u2,v2 '//' w,w1 ) ; ::_thesis: verum
end;
hence  ( u = u1 or v = v1 or u2,v2 '//' w,w1 ) by A2, A6; ::_thesis: verum
end;
hence  ( ( not AS is Euclidean_like & not AS is Minkowskian_like ) or AS is left_transitive ) by Def6, Def7, Def8; ::_thesis: verum
end;