let AS be Oriented_Orthogonality_Space; ( 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
;
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;
( 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
;
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 ( u = u1 implies u,u1 // v,v1 )set w = the
Element of
AS;
assume A9:
u = u1
;
u,u1 // v,v1consider 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;
verum end;
now ( u <> u1 implies u,u1 // v,v1 )assume
u <> u1
;
u,u1 // v,v1then
the
Element of
AS,
w1 '//' v,
v1
by A2, A3, A4, A5, A7;
hence
u,
u1 // v,
v1
by A6, A7;
verum end;
hence
u,
u1 // v,
v1
by A8;
verum
end;
assume A12:
AS is bach_transitive
; ( 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
;
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;
( 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
;
( w = w1 or v = v1 or u,u1 '//' u2,v2 )
now ( w <> w1 & v <> v1 & not w = w1 & not v = v1 implies u,u1 '//' u2,v2 )assume that A17:
w <> w1
and
v <> v1
;
( 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 )
;
hence
(
w = w1 or
v = v1 or
u,
u1 '//' u2,
v2 )
by A12, A14;
verum end;
hence
(
w = w1 or
v = v1 or
u,
u1 '//' u2,
v2 )
;
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; verum