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 A1: ( Gen x,y & AS = CESpace V,x,y ) ; :: thesis: ( AS is Euclidean_like & AS is left_transitive & AS is right_transitive & AS is bach_transitive )
A2: CESpace V,x,y = AffinStruct(# the carrier of V,(CORTE V,x,y) #) by ANALORT:def 7;

A3: 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 u' = u, v' = v, w' = w, u1' = u1, v1' = v1, w1' = w1, u2' = u2, v2' = v2 as Element of V by A1, A2;
( u',u1',v',v1' are_COrte_wrt x,y & w',w1',v',v1' are_COrte_wrt x,y & w',w1',u2',v2' are_COrte_wrt x,y & not w' = w1' & not v' = v1' implies u',u1',u2',v2' 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 A1, ANALORT:56; :: thesis: verum

end;

end;

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 u' = u, v' = v, w' = w, u1' = u1, v1' = v1, w1' = w1, u2' = u2, v2' = v2 as Element of V by A1, A2;
( u',u1',v',v1' are_COrte_wrt x,y & v',v1',w',w1' are_COrte_wrt x,y & u2',v2',w',w1' are_COrte_wrt x,y & not w' = w1' & not v' = v1' implies u',u1',u2',v2' 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 A1, ANALORT:56; :: thesis: verum

end;

end;

A5: 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 u' = u, v' = v, w' = w, u1' = u1, v1' = v1, w1' = w1, u2' = u2, v2' = v2 as Element of V by A1, A2;
( u',u1',v',v1' are_COrte_wrt x,y & v',v1',w',w1' are_COrte_wrt x,y & u',u1',u2',v2' are_COrte_wrt x,y & not u' = u1' & not v' = v1' implies u2',v2',w',w1' 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 A1, ANALORT:56; :: thesis: verum

end;

end;

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 u' = u, v' = v, u1' = u1, v1' = v1 as Element of V by A1, A2;
( u',u1',v',v1' are_COrte_wrt x,y implies v',v1',u1',u' are_COrte_wrt x,y ) by A1, ANALORT:18;
hence ( u,u1 '//' v,v1 implies v,v1 '//' u1,u ) by A1, ANALORT:56; :: thesis: verum

end;

end;

hence ( AS is Euclidean_like & AS is left_transitive & AS is right_transitive & AS is bach_transitive ) by A3, A4, A5, Def4, Def5, Def6, Def7; :: thesis: verum