:: AFVECT01 semantic presentation

begin

registration
let A be ( ( non empty ) ( non empty ) set ) ;
let C be ( ( ) ( ) Relation of ) ;
cluster AffinStruct(# A : ( ( non empty ) ( non empty ) set ) ,C : ( ( ) ( ) Element of bool [:[:A : ( ( non empty ) ( non empty ) set ) ,A : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,[:A : ( ( non empty ) ( non empty ) set ) ,A : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) #) : ( ( strict ) ( strict ) AffinStruct ) -> non empty strict ;
end;

definition
let IT be ( ( non empty ) ( non empty ) AffinStruct ) ;
attr IT is WeakAffSegm-like means :: AFVECT01:def 1
( ( for a, b being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) & ( for a, b being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) & ( for a, b, c, d, p, q being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) & ( for a, c being ( ( ) ( ) Element of ( ( ) ( ) set ) ) ex b being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) & ( for a, a9, b, b9, p being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> a9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> b9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // a9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) & ( for a, b being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) or ex c being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st
( ( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) or ex p, p9 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st
( p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> p9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,p9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,p9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // p9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ) ) ) & ( for a, b, b9, p, p9, c being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,p9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,p9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // p9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // b9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) & ( for a, b, b9, c being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> b9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // b9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
ex p, p9 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st
( p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> p9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,p9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,p9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // p9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ) & ( for a, b, c, p, p9, q, q9 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,p9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,q9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,p9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // p9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,q9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // q9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
ex r, r9 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st
( b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // r : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,r9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,r : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // r : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,r9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) // r9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ) );
end;

registration
cluster non empty non trivial strict WeakAffSegm-like for ( ( ) ( ) AffinStruct ) ;
end;

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

theorem :: AFVECT01:1
for AFV being ( ( non trivial WeakAffSegm-like ) ( non empty non trivial WeakAffSegm-like ) WeakAffSegm)
for a, b being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) holds a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ;

theorem :: AFVECT01:2
for AFV being ( ( non trivial WeakAffSegm-like ) ( non empty non trivial WeakAffSegm-like ) WeakAffSegm)
for a, b, c, d being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) holds
c : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ;

theorem :: AFVECT01:3
for AFV being ( ( non trivial WeakAffSegm-like ) ( non empty non trivial WeakAffSegm-like ) WeakAffSegm)
for a, b, c, d being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // d : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ;

theorem :: AFVECT01:4
for AFV being ( ( non trivial WeakAffSegm-like ) ( non empty non trivial WeakAffSegm-like ) WeakAffSegm)
for a, b, c, d being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) holds
b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ;

theorem :: AFVECT01:5
for AFV being ( ( non trivial WeakAffSegm-like ) ( non empty non trivial WeakAffSegm-like ) WeakAffSegm)
for a, b being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) holds a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ;

theorem :: AFVECT01:6
for AFV being ( ( non trivial WeakAffSegm-like ) ( non empty non trivial WeakAffSegm-like ) WeakAffSegm)
for a, b, c being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) = b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ;

theorem :: AFVECT01:7
for AFV being ( ( non trivial WeakAffSegm-like ) ( non empty non trivial WeakAffSegm-like ) WeakAffSegm)
for a, b, p, p9, c being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,p9 : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,p9 : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // p9 : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) = c : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ;

theorem :: AFVECT01:8
for AFV being ( ( non trivial WeakAffSegm-like ) ( non empty non trivial WeakAffSegm-like ) WeakAffSegm)
for a, b9, b99, b being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,b99 : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,b99 : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & not b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) = b9 : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & not b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) = b99 : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) holds
b9 : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) = b99 : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ;

definition
let AFV be ( ( non trivial WeakAffSegm-like ) ( non empty non trivial WeakAffSegm-like ) WeakAffSegm) ;
let a, b be ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ;
pred MDist a,b means :: AFVECT01:def 2
 ex p, p9 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st
( p : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) <> p9 : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & a : ( ( ) ( ) Element of bool [:[:AFV : ( ( V34() ) ( V34() ) set ) ,AFV : ( ( V34() ) ( V34() ) set ) :] : ( ( ) ( ) set ) ,[:AFV : ( ( V34() ) ( V34() ) set ) ,AFV : ( ( V34() ) ( V34() ) set ) :] : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of AFV : ( ( V34() ) ( V34() ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,p9 : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & a : ( ( ) ( ) Element of bool [:[:AFV : ( ( V34() ) ( V34() ) set ) ,AFV : ( ( V34() ) ( V34() ) set ) :] : ( ( ) ( ) set ) ,[:AFV : ( ( V34() ) ( V34() ) set ) ,AFV : ( ( V34() ) ( V34() ) set ) :] : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,b : ( ( ) ( ) Element of AFV : ( ( V34() ) ( V34() ) set ) ) & a : ( ( ) ( ) Element of bool [:[:AFV : ( ( V34() ) ( V34() ) set ) ,AFV : ( ( V34() ) ( V34() ) set ) :] : ( ( ) ( ) set ) ,[:AFV : ( ( V34() ) ( V34() ) set ) ,AFV : ( ( V34() ) ( V34() ) set ) :] : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,p9 : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // p9 : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,b : ( ( ) ( ) Element of AFV : ( ( V34() ) ( V34() ) set ) ) );
end;

definition
let AFV be ( ( non trivial WeakAffSegm-like ) ( non empty non trivial WeakAffSegm-like ) WeakAffSegm) ;
let a, b, c be ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ;
pred Mid a,b,c means :: AFVECT01:def 3
( ( a : ( ( ) ( ) Element of bool [:[:AFV : ( ( V34() ) ( V34() ) set ) ,AFV : ( ( V34() ) ( V34() ) set ) :] : ( ( ) ( ) set ) ,[:AFV : ( ( V34() ) ( V34() ) set ) ,AFV : ( ( V34() ) ( V34() ) set ) :] : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) = b : ( ( ) ( ) Element of AFV : ( ( V34() ) ( V34() ) set ) ) & b : ( ( ) ( ) Element of AFV : ( ( V34() ) ( V34() ) set ) ) = c : ( ( ) ( ) Element of the carrier of AFV : ( ( V34() ) ( V34() ) set ) : ( ( ) ( ) set ) ) & a : ( ( ) ( ) Element of bool [:[:AFV : ( ( V34() ) ( V34() ) set ) ,AFV : ( ( V34() ) ( V34() ) set ) :] : ( ( ) ( ) set ) ,[:AFV : ( ( V34() ) ( V34() ) set ) ,AFV : ( ( V34() ) ( V34() ) set ) :] : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) = c : ( ( ) ( ) Element of the carrier of AFV : ( ( V34() ) ( V34() ) set ) : ( ( ) ( ) set ) ) ) or ( a : ( ( ) ( ) Element of bool [:[:AFV : ( ( V34() ) ( V34() ) set ) ,AFV : ( ( V34() ) ( V34() ) set ) :] : ( ( ) ( ) set ) ,[:AFV : ( ( V34() ) ( V34() ) set ) ,AFV : ( ( V34() ) ( V34() ) set ) :] : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) = c : ( ( ) ( ) Element of the carrier of AFV : ( ( V34() ) ( V34() ) set ) : ( ( ) ( ) set ) ) & MDist a : ( ( ) ( ) Element of bool [:[:AFV : ( ( V34() ) ( V34() ) set ) ,AFV : ( ( V34() ) ( V34() ) set ) :] : ( ( ) ( ) set ) ,[:AFV : ( ( V34() ) ( V34() ) set ) ,AFV : ( ( V34() ) ( V34() ) set ) :] : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of AFV : ( ( V34() ) ( V34() ) set ) ) ) or ( a : ( ( ) ( ) Element of bool [:[:AFV : ( ( V34() ) ( V34() ) set ) ,AFV : ( ( V34() ) ( V34() ) set ) :] : ( ( ) ( ) set ) ,[:AFV : ( ( V34() ) ( V34() ) set ) ,AFV : ( ( V34() ) ( V34() ) set ) :] : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) <> c : ( ( ) ( ) Element of the carrier of AFV : ( ( V34() ) ( V34() ) set ) : ( ( ) ( ) set ) ) & a : ( ( ) ( ) Element of bool [:[:AFV : ( ( V34() ) ( V34() ) set ) ,AFV : ( ( V34() ) ( V34() ) set ) :] : ( ( ) ( ) set ) ,[:AFV : ( ( V34() ) ( V34() ) set ) ,AFV : ( ( V34() ) ( V34() ) set ) :] : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of AFV : ( ( V34() ) ( V34() ) set ) ) // b : ( ( ) ( ) Element of AFV : ( ( V34() ) ( V34() ) set ) ) ,c : ( ( ) ( ) Element of the carrier of AFV : ( ( V34() ) ( V34() ) set ) : ( ( ) ( ) set ) ) ) );
end;

theorem :: AFVECT01:9
for AFV being ( ( non trivial WeakAffSegm-like ) ( non empty non trivial WeakAffSegm-like ) WeakAffSegm)
for a, b being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & not MDist a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) holds
ex c being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) st
( a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) <> c : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ) ;

theorem :: AFVECT01:10
for AFV being ( ( non trivial WeakAffSegm-like ) ( non empty non trivial WeakAffSegm-like ) WeakAffSegm)
for a, b, c being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) st MDist a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) = c : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ;

theorem :: AFVECT01:11
for AFV being ( ( non trivial WeakAffSegm-like ) ( non empty non trivial WeakAffSegm-like ) WeakAffSegm)
for a, b being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) st MDist a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ;