:: 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;