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

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:46;
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:56; :: thesis: verum

end;

end;

A5: now

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:56; :: thesis: verum

end;

end;

A6: now

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:48;
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:56; :: thesis: verum

end;

end;

now

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