:: DIRORT semantic presentation

begin

notation
let AS be ( ( non empty ) ( non empty ) AffinStruct ) ;
let a, b, c, d be ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;
synonym a,b '//' c,d for a,b // c,d;
end;

theorem :: DIRORT:1
for V being ( ( non empty V67() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V67() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for x, y being ( ( ) ( ) VECTOR of ( ( ) ( ) set ) ) st Gen x : ( ( ) ( ) VECTOR of ( ( ) ( ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( ) set ) ) holds
( ( for u, u1, v, v1, w being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
( u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,w : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' w : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,w : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & ( u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & not u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) implies u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) & ( u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,w : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & not u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,w : ( ( ) ( ) Element of ( ( ) ( ) set ) ) implies u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' w : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) & ( u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) implies v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) & ( u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,w : ( ( ) ( ) Element of ( ( ) ( ) set ) ) implies u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,w : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) & ( not u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) or v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) or v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) ) ) & ( for u, v, w being ( ( ) ( ) Element of ( ( ) ( ) set ) ) ex u1 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st
( w : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & w : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) ) & ( for u, v, w being ( ( ) ( ) Element of ( ( ) ( ) set ) ) ex u1 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st
( w : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' w : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) ) ) ;

theorem :: DIRORT:2
for V being ( ( non empty V67() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V67() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for x, y being ( ( ) ( ) VECTOR of ( ( ) ( ) set ) ) st Gen x : ( ( ) ( ) VECTOR of ( ( ) ( ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( ) set ) ) holds
( ( for u, u1, v, v1, w being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
( u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,w : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' w : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,w : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & ( u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & not u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) implies u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) & ( u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,w : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & not u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,w : ( ( ) ( ) Element of ( ( ) ( ) set ) ) implies u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' w : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) & ( u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) implies v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) & ( u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,w : ( ( ) ( ) Element of ( ( ) ( ) set ) ) implies u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,w : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) & ( not u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) or v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) or v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) ) ) & ( for u, v, w being ( ( ) ( ) Element of ( ( ) ( ) set ) ) ex u1 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st
( w : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & w : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) ) & ( for u, v, w being ( ( ) ( ) Element of ( ( ) ( ) set ) ) ex u1 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st
( w : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' w : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) ) ) ;

definition
let IT be ( ( non empty ) ( non empty ) AffinStruct ) ;
attr IT is Oriented_Orthogonality_Space-like means :: DIRORT:def 1
( ( for u, u1, v, v1, w being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
( u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,w : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' w : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,w : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & ( u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & not u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) implies u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) & ( u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,w : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & not u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,w : ( ( ) ( ) Element of ( ( ) ( ) set ) ) implies u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' w : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) & ( u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) implies v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) & ( u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,w : ( ( ) ( ) Element of ( ( ) ( ) set ) ) implies u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,w : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) & ( not u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) or v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) or v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) ) ) & ( for u, v, w being ( ( ) ( ) Element of ( ( ) ( ) set ) ) ex u1 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st
( w : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & w : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) ) & ( for u, v, w being ( ( ) ( ) Element of ( ( ) ( ) set ) ) ex u1 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st
( w : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' w : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) ) );
end;

registration
cluster non empty Oriented_Orthogonality_Space-like for ( ( ) ( ) AffinStruct ) ;
end;

definition
mode Oriented_Orthogonality_Space is ( ( non empty Oriented_Orthogonality_Space-like ) ( non empty Oriented_Orthogonality_Space-like ) AffinStruct ) ;
end;

theorem :: DIRORT:3
for V being ( ( non empty V67() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V67() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for x, y being ( ( ) ( ) VECTOR of ( ( ) ( ) set ) ) st Gen x : ( ( ) ( ) VECTOR of ( ( ) ( ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( ) set ) ) holds
CMSpace (V : ( ( non empty V67() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V67() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ,x : ( ( ) ( ) VECTOR of ( ( ) ( ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty strict ) AffinStruct ) is ( ( non empty Oriented_Orthogonality_Space-like ) ( non empty Oriented_Orthogonality_Space-like ) Oriented_Orthogonality_Space) ;

theorem :: DIRORT:4
for V being ( ( non empty V67() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V67() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for x, y being ( ( ) ( ) VECTOR of ( ( ) ( ) set ) ) st Gen x : ( ( ) ( ) VECTOR of ( ( ) ( ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( ) set ) ) holds
CESpace (V : ( ( non empty V67() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V67() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ,x : ( ( ) ( ) VECTOR of ( ( ) ( ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty strict ) AffinStruct ) is ( ( non empty Oriented_Orthogonality_Space-like ) ( non empty Oriented_Orthogonality_Space-like ) Oriented_Orthogonality_Space) ;

theorem :: DIRORT:5
for AS being ( ( non empty Oriented_Orthogonality_Space-like ) ( non empty Oriented_Orthogonality_Space-like ) Oriented_Orthogonality_Space)
for u, v, w being ( ( ) ( ) Element of ( ( ) ( ) set ) ) ex u1 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st
( u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,w : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> w : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) ;

theorem :: DIRORT:6
for AS being ( ( non empty Oriented_Orthogonality_Space-like ) ( non empty Oriented_Orthogonality_Space-like ) Oriented_Orthogonality_Space)
for u, v, w being ( ( ) ( ) Element of ( ( ) ( ) set ) ) ex u1 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st
( u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & ( v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,w : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) or v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,w : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) ) ;

definition
let AS be ( ( non empty Oriented_Orthogonality_Space-like ) ( non empty Oriented_Orthogonality_Space-like ) Oriented_Orthogonality_Space) ;
let a, b, c, d be ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;
pred a,b _|_ c,d means :: DIRORT:def 2
( a : ( ( ) ( ) M2(K24(K25(K25(AS : ( ( ) ( ) ParOrtStr ) ,AS : ( ( ) ( ) ParOrtStr ) ) : ( ( ) ( ) set ) ,K25(AS : ( ( ) ( ) ParOrtStr ) ,AS : ( ( ) ( ) ParOrtStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ,b : ( ( ) ( ) M2(K24(K25(K25(AS : ( ( ) ( ) ParOrtStr ) ,AS : ( ( ) ( ) ParOrtStr ) ) : ( ( ) ( ) set ) ,K25(AS : ( ( ) ( ) ParOrtStr ) ,AS : ( ( ) ( ) ParOrtStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) '//' c : ( ( V12() V26(K25(K71() : ( ( ) ( ) set ) ,AS : ( ( ) ( ) ParOrtStr ) ) : ( ( ) ( ) set ) ,AS : ( ( ) ( ) ParOrtStr ) ) ) ( V12() V26(K25(K71() : ( ( ) ( ) set ) ,AS : ( ( ) ( ) ParOrtStr ) ) : ( ( ) ( ) set ) ,AS : ( ( ) ( ) ParOrtStr ) ) ) M2(K24(K25(K25(K71() : ( ( ) ( ) set ) ,AS : ( ( ) ( ) ParOrtStr ) ) : ( ( ) ( ) set ) ,AS : ( ( ) ( ) ParOrtStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ,d : ( ( ) ( ) M2( the carrier of AS : ( ( ) ( ) ParOrtStr ) : ( ( ) ( ) set ) )) or a : ( ( ) ( ) M2(K24(K25(K25(AS : ( ( ) ( ) ParOrtStr ) ,AS : ( ( ) ( ) ParOrtStr ) ) : ( ( ) ( ) set ) ,K25(AS : ( ( ) ( ) ParOrtStr ) ,AS : ( ( ) ( ) ParOrtStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ,b : ( ( ) ( ) M2(K24(K25(K25(AS : ( ( ) ( ) ParOrtStr ) ,AS : ( ( ) ( ) ParOrtStr ) ) : ( ( ) ( ) set ) ,K25(AS : ( ( ) ( ) ParOrtStr ) ,AS : ( ( ) ( ) ParOrtStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) '//' d : ( ( ) ( ) M2( the carrier of AS : ( ( ) ( ) ParOrtStr ) : ( ( ) ( ) set ) )) ,c : ( ( V12() V26(K25(K71() : ( ( ) ( ) set ) ,AS : ( ( ) ( ) ParOrtStr ) ) : ( ( ) ( ) set ) ,AS : ( ( ) ( ) ParOrtStr ) ) ) ( V12() V26(K25(K71() : ( ( ) ( ) set ) ,AS : ( ( ) ( ) ParOrtStr ) ) : ( ( ) ( ) set ) ,AS : ( ( ) ( ) ParOrtStr ) ) ) M2(K24(K25(K25(K71() : ( ( ) ( ) set ) ,AS : ( ( ) ( ) ParOrtStr ) ) : ( ( ) ( ) set ) ,AS : ( ( ) ( ) ParOrtStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) );
end;

definition
let AS be ( ( non empty Oriented_Orthogonality_Space-like ) ( non empty Oriented_Orthogonality_Space-like ) Oriented_Orthogonality_Space) ;
let a, b, c, d be ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;
pred a,b // c,d means :: DIRORT:def 3
 ex e, f being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st
( e : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> f : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & e : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,f : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' a : ( ( ) ( ) M2(K24(K25(K25(AS : ( ( ) ( ) ParOrtStr ) ,AS : ( ( ) ( ) ParOrtStr ) ) : ( ( ) ( ) set ) ,K25(AS : ( ( ) ( ) ParOrtStr ) ,AS : ( ( ) ( ) ParOrtStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ,b : ( ( ) ( ) M2(K24(K25(K25(AS : ( ( ) ( ) ParOrtStr ) ,AS : ( ( ) ( ) ParOrtStr ) ) : ( ( ) ( ) set ) ,K25(AS : ( ( ) ( ) ParOrtStr ) ,AS : ( ( ) ( ) ParOrtStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) & e : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,f : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' c : ( ( V12() V26(K25(K71() : ( ( ) ( ) set ) ,AS : ( ( ) ( ) ParOrtStr ) ) : ( ( ) ( ) set ) ,AS : ( ( ) ( ) ParOrtStr ) ) ) ( V12() V26(K25(K71() : ( ( ) ( ) set ) ,AS : ( ( ) ( ) ParOrtStr ) ) : ( ( ) ( ) set ) ,AS : ( ( ) ( ) ParOrtStr ) ) ) M2(K24(K25(K25(K71() : ( ( ) ( ) set ) ,AS : ( ( ) ( ) ParOrtStr ) ) : ( ( ) ( ) set ) ,AS : ( ( ) ( ) ParOrtStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ,d : ( ( ) ( ) M2( the carrier of AS : ( ( ) ( ) ParOrtStr ) : ( ( ) ( ) set ) )) );
end;

definition
let IT be ( ( non empty Oriented_Orthogonality_Space-like ) ( non empty Oriented_Orthogonality_Space-like ) Oriented_Orthogonality_Space) ;
attr IT is bach_transitive means :: DIRORT:def 4
 for u, u1, u2, v, v1, v2, w, w1 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & w : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,w1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & w : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,w1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' u2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & not w : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = w1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & not v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' u2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;
end;

definition
let IT be ( ( non empty Oriented_Orthogonality_Space-like ) ( non empty Oriented_Orthogonality_Space-like ) Oriented_Orthogonality_Space) ;
attr IT is right_transitive means :: DIRORT:def 5
 for u, u1, u2, v, v1, v2, w, w1 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' w : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,w1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & u2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' w : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,w1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & not w : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = w1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & not v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' u2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;
end;

definition
let IT be ( ( non empty Oriented_Orthogonality_Space-like ) ( non empty Oriented_Orthogonality_Space-like ) Oriented_Orthogonality_Space) ;
attr IT is left_transitive means :: DIRORT:def 6
 for u, u1, u2, v, v1, v2, w, w1 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' w : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,w1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' u2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & not u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & not v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
u2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' w : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,w1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;
end;

definition
let IT be ( ( non empty Oriented_Orthogonality_Space-like ) ( non empty Oriented_Orthogonality_Space-like ) Oriented_Orthogonality_Space) ;
attr IT is Euclidean_like means :: DIRORT:def 7
 for u, u1, v, v1 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;
end;

definition
let IT be ( ( non empty Oriented_Orthogonality_Space-like ) ( non empty Oriented_Orthogonality_Space-like ) Oriented_Orthogonality_Space) ;
attr IT is Minkowskian_like means :: DIRORT:def 8
 for u, u1, v, v1 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;
end;

theorem :: DIRORT:7
for AS being ( ( non empty Oriented_Orthogonality_Space-like ) ( non empty Oriented_Orthogonality_Space-like ) Oriented_Orthogonality_Space)
for u, u1, w being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
( u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) // w : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,w : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & w : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,w : ( ( ) ( ) Element of ( ( ) ( ) set ) ) // u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) ;

theorem :: DIRORT:8
for AS being ( ( non empty Oriented_Orthogonality_Space-like ) ( non empty Oriented_Orthogonality_Space-like ) Oriented_Orthogonality_Space)
for u, u1, v, v1 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) // v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) // u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;

theorem :: DIRORT:9
for AS being ( ( non empty Oriented_Orthogonality_Space-like ) ( non empty Oriented_Orthogonality_Space-like ) Oriented_Orthogonality_Space)
for u, u1, v, v1 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) // v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) // v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;

theorem :: DIRORT:10
for AS being ( ( non empty Oriented_Orthogonality_Space-like ) ( non empty Oriented_Orthogonality_Space-like ) Oriented_Orthogonality_Space) holds
( AS : ( ( non empty Oriented_Orthogonality_Space-like ) ( non empty Oriented_Orthogonality_Space-like ) Oriented_Orthogonality_Space) is left_transitive iff for v, v1, w, w1, u2, v2 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) // u2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' w : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,w1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
u2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' w : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,w1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) ;

theorem :: DIRORT:11
for AS being ( ( non empty Oriented_Orthogonality_Space-like ) ( non empty Oriented_Orthogonality_Space-like ) Oriented_Orthogonality_Space) holds
( AS : ( ( non empty Oriented_Orthogonality_Space-like ) ( non empty Oriented_Orthogonality_Space-like ) Oriented_Orthogonality_Space) is bach_transitive iff for u, u1, u2, v, v1, v2 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) // u2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' u2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) ;

theorem :: DIRORT:12
for AS being ( ( non empty Oriented_Orthogonality_Space-like ) ( non empty Oriented_Orthogonality_Space-like ) Oriented_Orthogonality_Space) st AS : ( ( non empty Oriented_Orthogonality_Space-like ) ( non empty Oriented_Orthogonality_Space-like ) Oriented_Orthogonality_Space) is bach_transitive holds
for u, u1, v, v1, w, w1 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) // v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) // w : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,w1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) // w : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,w1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;

theorem :: DIRORT:13
for V being ( ( non empty V67() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V67() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for x, y being ( ( ) ( ) VECTOR of ( ( ) ( ) set ) )
for AS being ( ( non empty Oriented_Orthogonality_Space-like ) ( non empty Oriented_Orthogonality_Space-like ) Oriented_Orthogonality_Space) st Gen x : ( ( ) ( ) VECTOR of ( ( ) ( ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( ) set ) ) & AS : ( ( non empty Oriented_Orthogonality_Space-like ) ( non empty Oriented_Orthogonality_Space-like ) Oriented_Orthogonality_Space) = CESpace (V : ( ( non empty V67() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V67() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ,x : ( ( ) ( ) VECTOR of ( ( ) ( ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty strict ) AffinStruct ) holds
( AS : ( ( non empty Oriented_Orthogonality_Space-like ) ( non empty Oriented_Orthogonality_Space-like ) Oriented_Orthogonality_Space) is Euclidean_like & AS : ( ( non empty Oriented_Orthogonality_Space-like ) ( non empty Oriented_Orthogonality_Space-like ) Oriented_Orthogonality_Space) is left_transitive & AS : ( ( non empty Oriented_Orthogonality_Space-like ) ( non empty Oriented_Orthogonality_Space-like ) Oriented_Orthogonality_Space) is right_transitive & AS : ( ( non empty Oriented_Orthogonality_Space-like ) ( non empty Oriented_Orthogonality_Space-like ) Oriented_Orthogonality_Space) is bach_transitive ) ;

registration
cluster non empty Oriented_Orthogonality_Space-like bach_transitive right_transitive left_transitive Euclidean_like for ( ( ) ( ) AffinStruct ) ;
end;

theorem :: DIRORT:14
for V being ( ( non empty V67() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V67() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for x, y being ( ( ) ( ) VECTOR of ( ( ) ( ) set ) )
for AS being ( ( non empty Oriented_Orthogonality_Space-like ) ( non empty Oriented_Orthogonality_Space-like ) Oriented_Orthogonality_Space) st Gen x : ( ( ) ( ) VECTOR of ( ( ) ( ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( ) set ) ) & AS : ( ( non empty Oriented_Orthogonality_Space-like ) ( non empty Oriented_Orthogonality_Space-like ) Oriented_Orthogonality_Space) = CMSpace (V : ( ( non empty V67() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V67() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ,x : ( ( ) ( ) VECTOR of ( ( ) ( ) set ) ) ,y : ( ( ) ( ) VECTOR of ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty strict ) AffinStruct ) holds
( AS : ( ( non empty Oriented_Orthogonality_Space-like ) ( non empty Oriented_Orthogonality_Space-like ) Oriented_Orthogonality_Space) is Minkowskian_like & AS : ( ( non empty Oriented_Orthogonality_Space-like ) ( non empty Oriented_Orthogonality_Space-like ) Oriented_Orthogonality_Space) is left_transitive & AS : ( ( non empty Oriented_Orthogonality_Space-like ) ( non empty Oriented_Orthogonality_Space-like ) Oriented_Orthogonality_Space) is right_transitive & AS : ( ( non empty Oriented_Orthogonality_Space-like ) ( non empty Oriented_Orthogonality_Space-like ) Oriented_Orthogonality_Space) is bach_transitive ) ;

registration
cluster non empty Oriented_Orthogonality_Space-like bach_transitive right_transitive left_transitive Minkowskian_like for ( ( ) ( ) AffinStruct ) ;
end;

theorem :: DIRORT:15
for AS being ( ( non empty Oriented_Orthogonality_Space-like ) ( non empty Oriented_Orthogonality_Space-like ) Oriented_Orthogonality_Space) st AS : ( ( non empty Oriented_Orthogonality_Space-like ) ( non empty Oriented_Orthogonality_Space-like ) Oriented_Orthogonality_Space) is left_transitive holds
AS : ( ( non empty Oriented_Orthogonality_Space-like ) ( non empty Oriented_Orthogonality_Space-like ) Oriented_Orthogonality_Space) is right_transitive ;

theorem :: DIRORT:16
for AS being ( ( non empty Oriented_Orthogonality_Space-like ) ( non empty Oriented_Orthogonality_Space-like ) Oriented_Orthogonality_Space) st AS : ( ( non empty Oriented_Orthogonality_Space-like ) ( non empty Oriented_Orthogonality_Space-like ) Oriented_Orthogonality_Space) is left_transitive holds
AS : ( ( non empty Oriented_Orthogonality_Space-like ) ( non empty Oriented_Orthogonality_Space-like ) Oriented_Orthogonality_Space) is bach_transitive ;

theorem :: DIRORT:17
for AS being ( ( non empty Oriented_Orthogonality_Space-like ) ( non empty Oriented_Orthogonality_Space-like ) Oriented_Orthogonality_Space) st AS : ( ( non empty Oriented_Orthogonality_Space-like ) ( non empty Oriented_Orthogonality_Space-like ) Oriented_Orthogonality_Space) is bach_transitive holds
( AS : ( ( non empty Oriented_Orthogonality_Space-like ) ( non empty Oriented_Orthogonality_Space-like ) Oriented_Orthogonality_Space) is right_transitive iff for u, u1, v, v1, u2, v2 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' u2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) '//' u2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & u2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> v2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,u1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) // v : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,v1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) ;

theorem :: DIRORT:18
for AS being ( ( non empty Oriented_Orthogonality_Space-like ) ( non empty Oriented_Orthogonality_Space-like ) Oriented_Orthogonality_Space) st AS : ( ( non empty Oriented_Orthogonality_Space-like ) ( non empty Oriented_Orthogonality_Space-like ) Oriented_Orthogonality_Space) is right_transitive & ( AS : ( ( non empty Oriented_Orthogonality_Space-like ) ( non empty Oriented_Orthogonality_Space-like ) Oriented_Orthogonality_Space) is Euclidean_like or AS : ( ( non empty Oriented_Orthogonality_Space-like ) ( non empty Oriented_Orthogonality_Space-like ) Oriented_Orthogonality_Space) is Minkowskian_like ) holds
AS : ( ( non empty Oriented_Orthogonality_Space-like ) ( non empty Oriented_Orthogonality_Space-like ) Oriented_Orthogonality_Space) is left_transitive ;