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 ) )
assume A1: 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, 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 ) 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

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 ) 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

assume A3: 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 A4: ( u,u1 '//' u2,v2 & v,v1 '//' u2,v2 & u2 <> v2 ) ; :: thesis: u,u1 // v,v1
consider w being Element of AS;
consider w1 being Element of AS such that
A5: ( w <> w1 & w,w1 '//' u,u1 ) by Def1;

A6: now

assume u <> u1 ; :: thesis: u,u1 // v,v1
then w,w1 '//' v,v1 by A3, A4, A5;
hence u,u1 // v,v1 by A5, Def3; :: thesis: verum

end;

now

assume A7: u = u1 ; :: thesis: u,u1 // v,v1
consider w being Element of AS;
consider w1 being Element of AS such that
A8: ( w <> w1 & w,w1 '//' v,v1 ) by Def1;
( w <> w1 & w,w1 '//' v,v1 & w,w1 '//' u,u ) by A8, Def1;
hence u,u1 // v,v1 by A7, Def3; :: thesis: verum

end;

hence u,u1 // v,v1 by A6; :: thesis: verum

end;

( ( 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 A9: 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 A10: ( u,u1 '//' v,v1 & v,v1 '//' w,w1 & u2,v2 '//' w,w1 ) ; :: thesis: ( w = w1 or v = v1 or u,u1 '//' u2,v2 )

now

assume ( w <> w1 & v <> v1 ) ; :: thesis: ( w = w1 or v = v1 or u,u1 '//' u2,v2 )
then v,v1 // u2,v2 by A9, A10;
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 A1, A10, Def4; :: thesis: verum

end;

hence ( w = w1 or v = v1 or u,u1 '//' u2,v2 ) ; :: thesis: verum

end;

hence ( ( 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 ) 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 A2; :: 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 Def5; :: thesis: verum