:: MIDSP_2 semantic presentation

begin

definition
let G be ( ( non empty ) ( non empty ) addLoopStr ) ;
let x be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
func Double x -> ( ( ) ( ) Element of ( ( ) ( ) set ) ) equals :: MIDSP_2:def 1
x : ( ( ) ( ) VectSpStr over G : ( ( ) ( ) MidStr ) ) + x : ( ( ) ( ) VectSpStr over G : ( ( ) ( ) MidStr ) ) : ( ( ) ( ) Element of the carrier of G : ( ( ) ( ) MidStr ) : ( ( ) ( ) set ) ) ;
end;

definition
let M be ( ( non empty ) ( non empty ) MidStr ) ;
let G be ( ( non empty ) ( non empty ) addLoopStr ) ;
let w be ( ( V6() V18([: the carrier of M : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of M : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of G : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([: the carrier of M : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of M : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of G : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([: the carrier of M : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of M : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of G : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [: the carrier of M : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of M : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of G : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ;
attr w is associating means :: MIDSP_2:def 2
 for p, q, r being ( ( ) ( ) Point of ( ( ) ( ) set ) ) holds
( p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) @ q : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of M : ( ( ) ( ) MidStr ) : ( ( ) ( ) set ) ) = r : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) iff w : ( ( V6() V18([:G : ( ( ) ( ) VectSpStr over M : ( ( ) ( ) MidStr ) ) ,G : ( ( ) ( ) VectSpStr over M : ( ( ) ( ) MidStr ) ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) VectSpStr over M : ( ( ) ( ) MidStr ) ) ) ) ( V1() V4([:G : ( ( ) ( ) VectSpStr over M : ( ( ) ( ) MidStr ) ) ,G : ( ( ) ( ) VectSpStr over M : ( ( ) ( ) MidStr ) ) :] : ( ( ) ( ) set ) ) V5(G : ( ( ) ( ) VectSpStr over M : ( ( ) ( ) MidStr ) ) ) V6() V18([:G : ( ( ) ( ) VectSpStr over M : ( ( ) ( ) MidStr ) ) ,G : ( ( ) ( ) VectSpStr over M : ( ( ) ( ) MidStr ) ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) VectSpStr over M : ( ( ) ( ) MidStr ) ) ) ) Element of bool [:[:G : ( ( ) ( ) VectSpStr over M : ( ( ) ( ) MidStr ) ) ,G : ( ( ) ( ) VectSpStr over M : ( ( ) ( ) MidStr ) ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) VectSpStr over M : ( ( ) ( ) MidStr ) ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) . (p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,r : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of G : ( ( ) ( ) VectSpStr over M : ( ( ) ( ) MidStr ) ) : ( ( ) ( ) set ) ) = w : ( ( V6() V18([:G : ( ( ) ( ) VectSpStr over M : ( ( ) ( ) MidStr ) ) ,G : ( ( ) ( ) VectSpStr over M : ( ( ) ( ) MidStr ) ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) VectSpStr over M : ( ( ) ( ) MidStr ) ) ) ) ( V1() V4([:G : ( ( ) ( ) VectSpStr over M : ( ( ) ( ) MidStr ) ) ,G : ( ( ) ( ) VectSpStr over M : ( ( ) ( ) MidStr ) ) :] : ( ( ) ( ) set ) ) V5(G : ( ( ) ( ) VectSpStr over M : ( ( ) ( ) MidStr ) ) ) V6() V18([:G : ( ( ) ( ) VectSpStr over M : ( ( ) ( ) MidStr ) ) ,G : ( ( ) ( ) VectSpStr over M : ( ( ) ( ) MidStr ) ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) VectSpStr over M : ( ( ) ( ) MidStr ) ) ) ) Element of bool [:[:G : ( ( ) ( ) VectSpStr over M : ( ( ) ( ) MidStr ) ) ,G : ( ( ) ( ) VectSpStr over M : ( ( ) ( ) MidStr ) ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) VectSpStr over M : ( ( ) ( ) MidStr ) ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) . (r : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,q : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of G : ( ( ) ( ) VectSpStr over M : ( ( ) ( ) MidStr ) ) : ( ( ) ( ) set ) ) );
end;

theorem :: MIDSP_2:1
for G being ( ( non empty ) ( non empty ) addLoopStr )
for M being ( ( non empty ) ( non empty ) MidStr )
for p being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for w being ( ( V6() V18([: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b1 : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [: the carrier of M : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of M : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of G : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) st w : ( ( V6() V18([: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b1 : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) is associating holds
p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) @ p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) ) = p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ;

definition
let S be ( ( non empty ) ( non empty ) set ) ;
let G be ( ( non empty ) ( non empty ) addLoopStr ) ;
let w be ( ( V6() V18([:S : ( ( non empty ) ( non empty ) set ) ,S : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of G : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([:S : ( ( non empty ) ( non empty ) set ) ,S : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of G : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([:S : ( ( non empty ) ( non empty ) set ) ,S : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of G : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [:S : ( ( non empty ) ( non empty ) set ) ,S : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of G : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ;
pred w is_atlas_of S,G means :: MIDSP_2:def 3
( ( for a being ( ( ) ( ) Element of S : ( ( ) ( ) MidStr ) )
for x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) ex b being ( ( ) ( ) Element of S : ( ( ) ( ) MidStr ) ) st w : ( ( V6() V18([:G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) ,G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) ) ) ( V1() V4([:G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) ,G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) :] : ( ( ) ( ) set ) ) V5(G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) ) V6() V18([:G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) ,G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) ) ) Element of bool [:[:G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) ,G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) . (a : ( ( ) ( ) Element of S : ( ( non empty ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of S : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) : ( ( ) ( ) set ) ) = x : ( ( ) ( ) Element of S : ( ( non empty ) ( non empty ) set ) ) ) & ( for a, b, c being ( ( ) ( ) Element of S : ( ( ) ( ) MidStr ) ) st w : ( ( V6() V18([:G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) ,G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) ) ) ( V1() V4([:G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) ,G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) :] : ( ( ) ( ) set ) ) V5(G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) ) V6() V18([:G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) ,G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) ) ) Element of bool [:[:G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) ,G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) . (a : ( ( ) ( ) Element of S : ( ( non empty ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of S : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) : ( ( ) ( ) set ) ) = w : ( ( V6() V18([:G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) ,G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) ) ) ( V1() V4([:G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) ,G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) :] : ( ( ) ( ) set ) ) V5(G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) ) V6() V18([:G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) ,G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) ) ) Element of bool [:[:G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) ,G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) . (a : ( ( ) ( ) Element of S : ( ( non empty ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of S : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) : ( ( ) ( ) set ) ) holds
b : ( ( ) ( ) Element of S : ( ( non empty ) ( non empty ) set ) ) = c : ( ( ) ( ) Element of S : ( ( non empty ) ( non empty ) set ) ) ) & ( for a, b, c being ( ( ) ( ) Element of S : ( ( ) ( ) MidStr ) ) holds (w : ( ( V6() V18([:G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) ,G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) ) ) ( V1() V4([:G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) ,G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) :] : ( ( ) ( ) set ) ) V5(G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) ) V6() V18([:G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) ,G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) ) ) Element of bool [:[:G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) ,G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) . (a : ( ( ) ( ) Element of S : ( ( non empty ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of S : ( ( non empty ) ( non empty ) set ) ) )) : ( ( ) ( ) Element of the carrier of G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) : ( ( ) ( ) set ) ) + (w : ( ( V6() V18([:G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) ,G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) ) ) ( V1() V4([:G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) ,G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) :] : ( ( ) ( ) set ) ) V5(G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) ) V6() V18([:G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) ,G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) ) ) Element of bool [:[:G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) ,G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) . (b : ( ( ) ( ) Element of S : ( ( non empty ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of S : ( ( non empty ) ( non empty ) set ) ) )) : ( ( ) ( ) Element of the carrier of G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) : ( ( ) ( ) set ) ) = w : ( ( V6() V18([:G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) ,G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) ) ) ( V1() V4([:G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) ,G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) :] : ( ( ) ( ) set ) ) V5(G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) ) V6() V18([:G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) ,G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) ) ) Element of bool [:[:G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) ,G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) . (a : ( ( ) ( ) Element of S : ( ( non empty ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of S : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) : ( ( ) ( ) set ) ) ) );
end;

definition
let S be ( ( non empty ) ( non empty ) set ) ;
let G be ( ( non empty ) ( non empty ) addLoopStr ) ;
let w be ( ( V6() V18([:S : ( ( non empty ) ( non empty ) set ) ,S : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of G : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([:S : ( ( non empty ) ( non empty ) set ) ,S : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of G : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([:S : ( ( non empty ) ( non empty ) set ) ,S : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of G : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [:S : ( ( non empty ) ( non empty ) set ) ,S : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of G : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ;
let a be ( ( ) ( ) Element of S : ( ( non empty ) ( non empty ) set ) ) ;
let x be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
assume w : ( ( V6() V18([:S : ( ( non empty ) ( non empty ) set ) ,S : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of G : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([:S : ( ( non empty ) ( non empty ) set ) ,S : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of G : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([:S : ( ( non empty ) ( non empty ) set ) ,S : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of G : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [:S : ( ( non empty ) ( non empty ) set ) ,S : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of G : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) is_atlas_of S : ( ( non empty ) ( non empty ) set ) ,G : ( ( non empty ) ( non empty ) addLoopStr ) ;
func (a,x) . w -> ( ( ) ( ) Element of S : ( ( ) ( ) MidStr ) ) means :: MIDSP_2:def 4
w : ( ( V6() V18([:G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) ,G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) ) ) ( V1() V4([:G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) ,G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) :] : ( ( ) ( ) set ) ) V5(G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) ) V6() V18([:G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) ,G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) ) ) Element of bool [:[:G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) ,G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) . (a : ( ( ) ( ) Element of G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) ) ,it : ( ( ) ( ) Element of S : ( ( ) ( ) MidStr ) ) ) : ( ( ) ( ) Element of the carrier of G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) : ( ( ) ( ) set ) ) = x : ( ( V6() V18([: the carrier of S : ( ( ) ( ) MidStr ) : ( ( ) ( ) set ) ,G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) ) ) ( V1() V4([: the carrier of S : ( ( ) ( ) MidStr ) : ( ( ) ( ) set ) ,G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) :] : ( ( ) ( ) set ) ) V5(G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) ) V6() V18([: the carrier of S : ( ( ) ( ) MidStr ) : ( ( ) ( ) set ) ,G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) ) ) Element of bool [:[: the carrier of S : ( ( ) ( ) MidStr ) : ( ( ) ( ) set ) ,G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) MidStr ) ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ;
end;

theorem :: MIDSP_2:2
for S being ( ( non empty ) ( non empty ) set )
for a being ( ( ) ( ) Element of S : ( ( non empty ) ( non empty ) set ) )
for G being ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr )
for w being ( ( V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b3 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b3 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b3 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [:S : ( ( non empty ) ( non empty ) set ) ,S : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) st w : ( ( V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b3 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b3 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b3 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b3 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) is_atlas_of S : ( ( non empty ) ( non empty ) set ) ,G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) holds
w : ( ( V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b3 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b3 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b3 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b3 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) . (a : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,a : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b3 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) = 0. G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( V49(b3 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) ) ) Element of the carrier of b3 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ;

theorem :: MIDSP_2:3
for S being ( ( non empty ) ( non empty ) set )
for a, b being ( ( ) ( ) Element of S : ( ( non empty ) ( non empty ) set ) )
for G being ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr )
for w being ( ( V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [:S : ( ( non empty ) ( non empty ) set ) ,S : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) st w : ( ( V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) is_atlas_of S : ( ( non empty ) ( non empty ) set ) ,G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) & w : ( ( V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) . (a : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) = 0. G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( V49(b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) ) ) Element of the carrier of b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) holds
a : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) = b : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: MIDSP_2:4
for S being ( ( non empty ) ( non empty ) set )
for a, b being ( ( ) ( ) Element of S : ( ( non empty ) ( non empty ) set ) )
for G being ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr )
for w being ( ( V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [:S : ( ( non empty ) ( non empty ) set ) ,S : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) st w : ( ( V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) is_atlas_of S : ( ( non empty ) ( non empty ) set ) ,G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) holds
w : ( ( V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) . (a : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) = - (w : ( ( V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) . (b : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,a : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) )) : ( ( ) ( ) Element of the carrier of b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ;

theorem :: MIDSP_2:5
for S being ( ( non empty ) ( non empty ) set )
for a, b, c, d being ( ( ) ( ) Element of S : ( ( non empty ) ( non empty ) set ) )
for G being ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr )
for w being ( ( V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b6 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b6 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b6 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [:S : ( ( non empty ) ( non empty ) set ) ,S : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) st w : ( ( V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b6 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b6 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b6 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b6 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) is_atlas_of S : ( ( non empty ) ( non empty ) set ) ,G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) & w : ( ( V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b6 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b6 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b6 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b6 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) . (a : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b6 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) = w : ( ( V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b6 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b6 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b6 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b6 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) . (c : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,d : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b6 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) holds
w : ( ( V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b6 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b6 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b6 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b6 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) . (b : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,a : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b6 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) = w : ( ( V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b6 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b6 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b6 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b6 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) . (d : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b6 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ;

theorem :: MIDSP_2:6
for S being ( ( non empty ) ( non empty ) set )
for G being ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr )
for w being ( ( V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [:S : ( ( non empty ) ( non empty ) set ) ,S : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) st w : ( ( V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) is_atlas_of S : ( ( non empty ) ( non empty ) set ) ,G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) holds
for b being ( ( ) ( ) Element of S : ( ( non empty ) ( non empty ) set ) )
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ex a being ( ( ) ( ) Element of S : ( ( non empty ) ( non empty ) set ) ) st w : ( ( V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) . (a : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: MIDSP_2:7
for S being ( ( non empty ) ( non empty ) set )
for b, a, c being ( ( ) ( ) Element of S : ( ( non empty ) ( non empty ) set ) )
for G being ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr )
for w being ( ( V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b5 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b5 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b5 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [:S : ( ( non empty ) ( non empty ) set ) ,S : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) st w : ( ( V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b5 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b5 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b5 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b5 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) is_atlas_of S : ( ( non empty ) ( non empty ) set ) ,G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) & w : ( ( V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b5 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b5 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b5 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b5 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) . (b : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,a : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b5 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) = w : ( ( V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b5 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b5 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b5 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b5 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) . (c : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,a : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b5 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) holds
b : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) = c : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: MIDSP_2:8
for M being ( ( non empty ) ( non empty ) MidStr )
for p, q being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for G being ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr )
for w being ( ( V6() V18([: the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([: the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([: the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [: the carrier of M : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of M : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) st w : ( ( V6() V18([: the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([: the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([: the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [: the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) is_atlas_of the carrier of M : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) ,G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) & w : ( ( V6() V18([: the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([: the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([: the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [: the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) is associating holds
p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) @ q : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) ) = q : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) @ p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) ) ;

theorem :: MIDSP_2:9
for M being ( ( non empty ) ( non empty ) MidStr )
for p, q being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for G being ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr )
for w being ( ( V6() V18([: the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([: the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([: the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [: the carrier of M : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of M : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) st w : ( ( V6() V18([: the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([: the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([: the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [: the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) is_atlas_of the carrier of M : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) ,G : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) & w : ( ( V6() V18([: the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([: the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([: the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [: the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b4 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) is associating holds
ex r being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st r : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) @ p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) ) = q : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ;

theorem :: MIDSP_2:10
for G being ( ( non empty Abelian add-associative ) ( non empty Abelian add-associative ) addLoopStr )
for x, y, z, t being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) + y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Abelian add-associative ) ( non empty Abelian add-associative ) addLoopStr ) : ( ( ) ( non empty ) set ) ) + (z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) + t : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Abelian add-associative ) ( non empty Abelian add-associative ) addLoopStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Abelian add-associative ) ( non empty Abelian add-associative ) addLoopStr ) : ( ( ) ( non empty ) set ) ) = (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) + z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Abelian add-associative ) ( non empty Abelian add-associative ) addLoopStr ) : ( ( ) ( non empty ) set ) ) + (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) + t : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Abelian add-associative ) ( non empty Abelian add-associative ) addLoopStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Abelian add-associative ) ( non empty Abelian add-associative ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ;

theorem :: MIDSP_2:11
for G being ( ( non empty Abelian add-associative ) ( non empty Abelian add-associative ) addLoopStr )
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds Double (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) + y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Abelian add-associative ) ( non empty Abelian add-associative ) addLoopStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = (Double x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) + (Double y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Abelian add-associative ) ( non empty Abelian add-associative ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ;

theorem :: MIDSP_2:12
for G being ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr )
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds Double (- x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = - (Double x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ;

theorem :: MIDSP_2:13
for M being ( ( non empty ) ( non empty ) MidStr )
for G being ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr )
for w being ( ( V6() V18([: the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([: the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([: the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [: the carrier of M : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of M : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of G : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) st w : ( ( V6() V18([: the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([: the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([: the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [: the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) is_atlas_of the carrier of M : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) ,G : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) & w : ( ( V6() V18([: the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([: the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([: the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [: the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) is associating holds
for a, b, c, d being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds
( a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) @ b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) ) = c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) @ d : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) ) iff w : ( ( V6() V18([: the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([: the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([: the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [: the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) . (a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,d : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) = w : ( ( V6() V18([: the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([: the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([: the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [: the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) . (c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: MIDSP_2:14
for S being ( ( non empty ) ( non empty ) set )
for G being ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr )
for w being ( ( V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [:S : ( ( non empty ) ( non empty ) set ) ,S : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of G : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) st w : ( ( V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) is_atlas_of S : ( ( non empty ) ( non empty ) set ) ,G : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) holds
for a, b, b9, c, c9 being ( ( ) ( ) Element of S : ( ( non empty ) ( non empty ) set ) ) st w : ( ( V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) . (a : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) = w : ( ( V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) . (b : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) & w : ( ( V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) . (a : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,b9 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) = w : ( ( V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) . (b9 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,c9 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) holds
w : ( ( V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) . (c : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,c9 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) = Double (w : ( ( V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) . (b : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,b9 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) )) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

registration
let M be ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ;
cluster vectgroup M : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidStr ) : ( ( ) ( non empty strict ) addLoopStr ) -> right_complementable Abelian add-associative right_zeroed ;
end;

theorem :: MIDSP_2:15
for M being ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) holds
( ( for a being ( ( ) ( ) set ) holds
( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) iff a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is ( ( ) ( V1() V4( the carrier of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) : ( ( ) ( non empty ) set ) ) V5( the carrier of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) : ( ( ) ( non empty ) set ) ) non empty ) Vector of M : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) ) ) & 0. (vectgroup M : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) : ( ( ) ( non empty strict right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( V49( vectgroup b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) : ( ( ) ( non empty strict right_complementable Abelian add-associative right_zeroed ) addLoopStr ) ) ) Element of the carrier of (vectgroup b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) : ( ( ) ( non empty strict right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) = ID M : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) : ( ( ) ( V1() V4( the carrier of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) : ( ( ) ( non empty ) set ) ) V5( the carrier of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) : ( ( ) ( non empty ) set ) ) non empty ) Vector of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) & ( for a, b being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for x, y being ( ( ) ( V1() V4( the carrier of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) : ( ( ) ( non empty ) set ) ) V5( the carrier of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) : ( ( ) ( non empty ) set ) ) non empty ) Vector of M : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = x : ( ( ) ( V1() V4( the carrier of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) : ( ( ) ( non empty ) set ) ) V5( the carrier of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) : ( ( ) ( non empty ) set ) ) non empty ) Vector of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) & b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = y : ( ( ) ( V1() V4( the carrier of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) : ( ( ) ( non empty ) set ) ) V5( the carrier of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) : ( ( ) ( non empty ) set ) ) non empty ) Vector of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) holds
a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) + b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (vectgroup b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) : ( ( ) ( non empty strict right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) = x : ( ( ) ( V1() V4( the carrier of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) : ( ( ) ( non empty ) set ) ) V5( the carrier of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) : ( ( ) ( non empty ) set ) ) non empty ) Vector of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) + y : ( ( ) ( V1() V4( the carrier of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) : ( ( ) ( non empty ) set ) ) V5( the carrier of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) : ( ( ) ( non empty ) set ) ) non empty ) Vector of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) : ( ( ) ( V1() V4( the carrier of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) : ( ( ) ( non empty ) set ) ) V5( the carrier of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) : ( ( ) ( non empty ) set ) ) non empty ) Vector of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) ) ) ;

definition
let IT be ( ( non empty ) ( non empty ) addLoopStr ) ;
attr IT is midpoint_operator means :: MIDSP_2:def 5
( ( for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ex x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st Double x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) & ( for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st Double a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = 0. IT : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( V49(IT : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ) Element of the carrier of IT : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = 0. IT : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( V49(IT : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ) Element of the carrier of IT : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) ) );
end;

registration
cluster non empty midpoint_operator -> non empty Fanoian for ( ( ) ( ) addLoopStr ) ;
end;

registration
cluster non empty strict right_complementable Abelian add-associative right_zeroed midpoint_operator for ( ( ) ( ) addLoopStr ) ;
end;

theorem :: MIDSP_2:16
for G being ( ( non empty right_complementable Fanoian add-associative right_zeroed ) ( non empty right_complementable Fanoian add-associative right_zeroed ) addLoopStr )
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = - x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty right_complementable Fanoian add-associative right_zeroed ) ( non empty right_complementable Fanoian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) holds
x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = 0. G : ( ( non empty right_complementable Fanoian add-associative right_zeroed ) ( non empty right_complementable Fanoian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( V49(b1 : ( ( non empty right_complementable Fanoian add-associative right_zeroed ) ( non empty right_complementable Fanoian add-associative right_zeroed ) addLoopStr ) ) ) Element of the carrier of b1 : ( ( non empty right_complementable Fanoian add-associative right_zeroed ) ( non empty right_complementable Fanoian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ;

theorem :: MIDSP_2:17
for G being ( ( non empty right_complementable Fanoian Abelian add-associative right_zeroed ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed ) addLoopStr )
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st Double x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = Double y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

definition
let G be ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) ;
let x be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
func Half x -> ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) means :: MIDSP_2:def 6
 Double it : ( ( V6() V18([:x : ( ( ) ( ) set ) ,x : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,x : ( ( ) ( ) set ) ) ) ( V1() V4([:x : ( ( ) ( ) set ) ,x : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ) V5(x : ( ( ) ( ) set ) ) V6() V18([:x : ( ( ) ( ) set ) ,x : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,x : ( ( ) ( ) set ) ) ) Element of bool [:[:x : ( ( ) ( ) set ) ,x : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,x : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) set ) ;
end;

theorem :: MIDSP_2:18
for G being ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr )
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( Half (0. G : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) ) : ( ( ) ( V49(b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) ) ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = 0. G : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( V49(b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) ) ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) & Half (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) + y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = (Half x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) + (Half y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) & ( Half x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = Half y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) implies x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) & Half (Double x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ;

theorem :: MIDSP_2:19
for G being ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr )
for M being ( ( non empty ) ( non empty ) MidStr )
for w being ( ( V6() V18([: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [: the carrier of M : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of M : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of G : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) st w : ( ( V6() V18([: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) is_atlas_of the carrier of M : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) ,G : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) & w : ( ( V6() V18([: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) is associating holds
for a, b, c, d being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds (a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) @ b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) ) @ (c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) @ d : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) ) = (a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) @ c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) ) @ (b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) @ d : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) ) ;

theorem :: MIDSP_2:20
for G being ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr )
for M being ( ( non empty ) ( non empty ) MidStr )
for w being ( ( V6() V18([: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [: the carrier of M : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of M : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of G : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) st w : ( ( V6() V18([: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) is_atlas_of the carrier of M : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) ,G : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) & w : ( ( V6() V18([: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) is associating holds
M : ( ( non empty ) ( non empty ) MidStr ) is ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ;

registration
let M be ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ;
cluster vectgroup M : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidStr ) : ( ( ) ( non empty strict right_complementable Abelian add-associative right_zeroed ) addLoopStr ) -> midpoint_operator ;
end;

definition
let M be ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ;
let p, q be ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ;
func vector (p,q) -> ( ( ) ( ) Element of ( ( ) ( ) set ) ) equals :: MIDSP_2:def 7
 vect (p : ( ( ) ( ) set ) ,q : ( ( V6() V18([:p : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) ) ) ( V1() V4([:p : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ) V5(p : ( ( ) ( ) set ) ) V6() V18([:p : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) ) ) Element of bool [:[:p : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4( the carrier of M : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) V5( the carrier of M : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) non empty ) Vector of M : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ;
end;

definition
let M be ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ;
func vect M -> ( ( V6() V18([: the carrier of M : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of M : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of (vectgroup M : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) : ( ( ) ( ) addLoopStr ) : ( ( ) ( ) set ) ) ) ( V1() V4([: the carrier of M : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of M : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of (vectgroup M : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) : ( ( ) ( ) addLoopStr ) : ( ( ) ( ) set ) ) V6() V18([: the carrier of M : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of M : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of (vectgroup M : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) : ( ( ) ( ) addLoopStr ) : ( ( ) ( ) set ) ) ) Function of [: the carrier of M : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of M : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of (vectgroup M : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) : ( ( ) ( ) addLoopStr ) : ( ( ) ( ) set ) ) means :: MIDSP_2:def 8
 for p, q being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds it : ( ( ) ( ) set ) . (p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,q : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of (vectgroup M : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) : ( ( ) ( ) addLoopStr ) : ( ( ) ( ) set ) ) = vect (p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,q : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V1() V4( the carrier of M : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) V5( the carrier of M : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) non empty ) Vector of M : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ;
end;

theorem :: MIDSP_2:21
for M being ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) holds vect M : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) : ( ( V6() V18([: the carrier of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of (vectgroup b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) : ( ( ) ( non empty strict right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([: the carrier of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of (vectgroup b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) : ( ( ) ( non empty strict right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([: the carrier of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of (vectgroup b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) : ( ( ) ( non empty strict right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [: the carrier of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of (vectgroup b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) : ( ( ) ( non empty strict right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) is_atlas_of the carrier of M : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) : ( ( ) ( non empty ) set ) , vectgroup M : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) : ( ( ) ( non empty strict right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) ;

theorem :: MIDSP_2:22
for M being ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp)
for p, q, r, s being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds
( vect (p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,q : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V1() V4( the carrier of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) : ( ( ) ( non empty ) set ) ) V5( the carrier of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) : ( ( ) ( non empty ) set ) ) non empty ) Vector of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) = vect (r : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,s : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V1() V4( the carrier of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) : ( ( ) ( non empty ) set ) ) V5( the carrier of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) : ( ( ) ( non empty ) set ) ) non empty ) Vector of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) iff p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) @ s : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) : ( ( ) ( non empty ) set ) ) = q : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) @ r : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: MIDSP_2:23
for M being ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp)
for p, q, r being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds
( p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) @ q : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) : ( ( ) ( non empty ) set ) ) = r : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) iff vect (p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,r : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V1() V4( the carrier of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) : ( ( ) ( non empty ) set ) ) V5( the carrier of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) : ( ( ) ( non empty ) set ) ) non empty ) Vector of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) = vect (r : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,q : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V1() V4( the carrier of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) : ( ( ) ( non empty ) set ) ) V5( the carrier of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) : ( ( ) ( non empty ) set ) ) non empty ) Vector of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) ) ;

theorem :: MIDSP_2:24
canceled;

registration
let M be ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ;
cluster vect M : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidStr ) : ( ( V6() V18([: the carrier of M : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of M : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of (vectgroup M : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidStr ) ) : ( ( ) ( non empty strict right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([: the carrier of M : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of M : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of (vectgroup M : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidStr ) ) : ( ( ) ( non empty strict right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([: the carrier of M : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of M : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of (vectgroup M : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidStr ) ) : ( ( ) ( non empty strict right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [: the carrier of M : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of M : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of (vectgroup M : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidStr ) ) : ( ( ) ( non empty strict right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) -> V6() V18([: the carrier of M : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of M : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of (vectgroup M : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidStr ) ) : ( ( ) ( non empty strict right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) associating ;
end;

definition
let S be ( ( non empty ) ( non empty ) set ) ;
let G be ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) ;
let w be ( ( V6() V18([:S : ( ( non empty ) ( non empty ) set ) ,S : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of G : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([:S : ( ( non empty ) ( non empty ) set ) ,S : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of G : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([:S : ( ( non empty ) ( non empty ) set ) ,S : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of G : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [:S : ( ( non empty ) ( non empty ) set ) ,S : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of G : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ;
assume w : ( ( V6() V18([:S : ( ( non empty ) ( non empty ) set ) ,S : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of G : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([:S : ( ( non empty ) ( non empty ) set ) ,S : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of G : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([:S : ( ( non empty ) ( non empty ) set ) ,S : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of G : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [:S : ( ( non empty ) ( non empty ) set ) ,S : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of G : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) is_atlas_of S : ( ( non empty ) ( non empty ) set ) ,G : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) ;
func @ w -> ( ( V6() V18([:S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ,S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) :] : ( ( ) ( ) set ) ,S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ) ( V1() V4([:S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ,S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) :] : ( ( ) ( ) set ) ) V5(S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) V6() V18([:S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ,S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) :] : ( ( ) ( ) set ) ,S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ) BinOp of S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) means :: MIDSP_2:def 9
 for a, b being ( ( ) ( ) Element of S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) holds w : ( ( V6() V18([:G : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) ) ) ( V1() V4([:G : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ) V5(G : ( ( ) ( ) set ) ) V6() V18([:G : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) ) ) Element of bool [:[:G : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) . (a : ( ( ) ( ) Element of S : ( ( non empty ) ( non empty ) set ) ) ,(it : ( ( ) ( ) Element of G : ( ( ) ( ) set ) ) . (a : ( ( ) ( ) Element of S : ( ( non empty ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of S : ( ( non empty ) ( non empty ) set ) ) )) : ( ( ) ( ) Element of S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ) : ( ( ) ( ) Element of the carrier of G : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) = w : ( ( V6() V18([:G : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) ) ) ( V1() V4([:G : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ) V5(G : ( ( ) ( ) set ) ) V6() V18([:G : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) ) ) Element of bool [:[:G : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) . ((it : ( ( ) ( ) Element of G : ( ( ) ( ) set ) ) . (a : ( ( ) ( ) Element of S : ( ( non empty ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of S : ( ( non empty ) ( non empty ) set ) ) )) : ( ( ) ( ) Element of S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ,b : ( ( ) ( ) Element of S : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of G : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ;
end;

theorem :: MIDSP_2:25
for S being ( ( non empty ) ( non empty ) set )
for G being ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr )
for w being ( ( V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [:S : ( ( non empty ) ( non empty ) set ) ,S : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of G : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) st w : ( ( V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) is_atlas_of S : ( ( non empty ) ( non empty ) set ) ,G : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) holds
for a, b, c being ( ( ) ( ) Element of S : ( ( non empty ) ( non empty ) set ) ) holds
( (@ w : ( ( V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) : ( ( V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5(b1 : ( ( non empty ) ( non empty ) set ) ) V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) BinOp of b1 : ( ( non empty ) ( non empty ) set ) ) . (a : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) = c : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) iff w : ( ( V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) . (a : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) = w : ( ( V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) . (c : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ;

registration
let D be ( ( non empty ) ( non empty ) set ) ;
let M be ( ( V6() V18([:D : ( ( non empty ) ( non empty ) set ) ,D : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,D : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4([:D : ( ( non empty ) ( non empty ) set ) ,D : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5(D : ( ( non empty ) ( non empty ) set ) ) V6() V18([:D : ( ( non empty ) ( non empty ) set ) ,D : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,D : ( ( non empty ) ( non empty ) set ) ) ) BinOp of D : ( ( non empty ) ( non empty ) set ) ) ;
cluster MidStr(# D : ( ( non empty ) ( non empty ) set ) ,M : ( ( V6() V18([:D : ( ( non empty ) ( non empty ) set ) ,D : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,D : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4([:D : ( ( non empty ) ( non empty ) set ) ,D : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5(D : ( ( non empty ) ( non empty ) set ) ) V6() V18([:D : ( ( non empty ) ( non empty ) set ) ,D : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,D : ( ( non empty ) ( non empty ) set ) ) ) Element of bool [:[:D : ( ( non empty ) ( non empty ) set ) ,D : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,D : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) #) : ( ( strict ) ( strict ) MidStr ) -> non empty strict ;
end;

definition
let S be ( ( non empty ) ( non empty ) set ) ;
let G be ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) ;
let w be ( ( V6() V18([:S : ( ( non empty ) ( non empty ) set ) ,S : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of G : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([:S : ( ( non empty ) ( non empty ) set ) ,S : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of G : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([:S : ( ( non empty ) ( non empty ) set ) ,S : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of G : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [:S : ( ( non empty ) ( non empty ) set ) ,S : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of G : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ;
func Atlas w -> ( ( V6() V18([: the carrier of MidStr(# S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ,(@ w : ( ( V6() V18([:G : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) ) ) ( V1() V4([:G : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ) V5(G : ( ( ) ( ) set ) ) V6() V18([:G : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) ) ) Element of bool [:[:G : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( ( V6() V18([:S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ,S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) :] : ( ( ) ( ) set ) ,S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ) ( V1() V4([:S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ,S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) :] : ( ( ) ( ) set ) ) V5(S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) V6() V18([:S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ,S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) :] : ( ( ) ( ) set ) ,S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ) BinOp of S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) #) : ( ( strict ) ( strict ) MidStr ) : ( ( ) ( ) set ) , the carrier of MidStr(# S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ,(@ w : ( ( V6() V18([:G : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) ) ) ( V1() V4([:G : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ) V5(G : ( ( ) ( ) set ) ) V6() V18([:G : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) ) ) Element of bool [:[:G : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( ( V6() V18([:S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ,S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) :] : ( ( ) ( ) set ) ,S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ) ( V1() V4([:S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ,S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) :] : ( ( ) ( ) set ) ) V5(S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) V6() V18([:S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ,S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) :] : ( ( ) ( ) set ) ,S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ) BinOp of S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) #) : ( ( strict ) ( strict ) MidStr ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of G : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ( V1() V4([: the carrier of MidStr(# S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ,(@ w : ( ( V6() V18([:G : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) ) ) ( V1() V4([:G : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ) V5(G : ( ( ) ( ) set ) ) V6() V18([:G : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) ) ) Element of bool [:[:G : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( ( V6() V18([:S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ,S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) :] : ( ( ) ( ) set ) ,S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ) ( V1() V4([:S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ,S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) :] : ( ( ) ( ) set ) ) V5(S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) V6() V18([:S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ,S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) :] : ( ( ) ( ) set ) ,S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ) BinOp of S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) #) : ( ( strict ) ( strict ) MidStr ) : ( ( ) ( ) set ) , the carrier of MidStr(# S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ,(@ w : ( ( V6() V18([:G : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) ) ) ( V1() V4([:G : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ) V5(G : ( ( ) ( ) set ) ) V6() V18([:G : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) ) ) Element of bool [:[:G : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( ( V6() V18([:S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ,S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) :] : ( ( ) ( ) set ) ,S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ) ( V1() V4([:S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ,S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) :] : ( ( ) ( ) set ) ) V5(S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) V6() V18([:S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ,S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) :] : ( ( ) ( ) set ) ,S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ) BinOp of S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) #) : ( ( strict ) ( strict ) MidStr ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of G : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) V6() V18([: the carrier of MidStr(# S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ,(@ w : ( ( V6() V18([:G : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) ) ) ( V1() V4([:G : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ) V5(G : ( ( ) ( ) set ) ) V6() V18([:G : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) ) ) Element of bool [:[:G : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( ( V6() V18([:S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ,S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) :] : ( ( ) ( ) set ) ,S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ) ( V1() V4([:S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ,S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) :] : ( ( ) ( ) set ) ) V5(S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) V6() V18([:S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ,S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) :] : ( ( ) ( ) set ) ,S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ) BinOp of S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) #) : ( ( strict ) ( strict ) MidStr ) : ( ( ) ( ) set ) , the carrier of MidStr(# S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ,(@ w : ( ( V6() V18([:G : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) ) ) ( V1() V4([:G : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ) V5(G : ( ( ) ( ) set ) ) V6() V18([:G : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) ) ) Element of bool [:[:G : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( ( V6() V18([:S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ,S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) :] : ( ( ) ( ) set ) ,S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ) ( V1() V4([:S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ,S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) :] : ( ( ) ( ) set ) ) V5(S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) V6() V18([:S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ,S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) :] : ( ( ) ( ) set ) ,S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ) BinOp of S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) #) : ( ( strict ) ( strict ) MidStr ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of G : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) Function of [: the carrier of MidStr(# S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ,(@ w : ( ( V6() V18([:G : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) ) ) ( V1() V4([:G : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ) V5(G : ( ( ) ( ) set ) ) V6() V18([:G : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) ) ) Element of bool [:[:G : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( ( V6() V18([:S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ,S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) :] : ( ( ) ( ) set ) ,S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ) ( V1() V4([:S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ,S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) :] : ( ( ) ( ) set ) ) V5(S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) V6() V18([:S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ,S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) :] : ( ( ) ( ) set ) ,S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ) BinOp of S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) #) : ( ( strict ) ( strict ) MidStr ) : ( ( ) ( ) set ) , the carrier of MidStr(# S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ,(@ w : ( ( V6() V18([:G : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) ) ) ( V1() V4([:G : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ) V5(G : ( ( ) ( ) set ) ) V6() V18([:G : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) ) ) Element of bool [:[:G : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( ( V6() V18([:S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ,S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) :] : ( ( ) ( ) set ) ,S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ) ( V1() V4([:S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ,S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) :] : ( ( ) ( ) set ) ) V5(S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) V6() V18([:S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ,S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) :] : ( ( ) ( ) set ) ,S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ) BinOp of S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) #) : ( ( strict ) ( strict ) MidStr ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of G : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) equals :: MIDSP_2:def 10
w : ( ( V6() V18([:G : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) ) ) ( V1() V4([:G : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ) V5(G : ( ( ) ( ) set ) ) V6() V18([:G : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) ) ) Element of bool [:[:G : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ;
end;

theorem :: MIDSP_2:26
for S being ( ( non empty ) ( non empty ) set )
for G being ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr )
for w being ( ( V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [:S : ( ( non empty ) ( non empty ) set ) ,S : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of G : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) st w : ( ( V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) is_atlas_of S : ( ( non empty ) ( non empty ) set ) ,G : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) holds
Atlas w : ( ( V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) : ( ( V6() V18([: the carrier of MidStr(# b1 : ( ( non empty ) ( non empty ) set ) ,(@ b3 : ( ( V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) : ( ( V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5(b1 : ( ( non empty ) ( non empty ) set ) ) V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) BinOp of b1 : ( ( non empty ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of MidStr(# b1 : ( ( non empty ) ( non empty ) set ) ,(@ b3 : ( ( V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) : ( ( V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5(b1 : ( ( non empty ) ( non empty ) set ) ) V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) BinOp of b1 : ( ( non empty ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([: the carrier of MidStr(# b1 : ( ( non empty ) ( non empty ) set ) ,(@ b3 : ( ( V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) : ( ( V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5(b1 : ( ( non empty ) ( non empty ) set ) ) V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) BinOp of b1 : ( ( non empty ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of MidStr(# b1 : ( ( non empty ) ( non empty ) set ) ,(@ b3 : ( ( V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) : ( ( V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5(b1 : ( ( non empty ) ( non empty ) set ) ) V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) BinOp of b1 : ( ( non empty ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([: the carrier of MidStr(# b1 : ( ( non empty ) ( non empty ) set ) ,(@ b3 : ( ( V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) : ( ( V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5(b1 : ( ( non empty ) ( non empty ) set ) ) V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) BinOp of b1 : ( ( non empty ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of MidStr(# b1 : ( ( non empty ) ( non empty ) set ) ,(@ b3 : ( ( V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) : ( ( V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5(b1 : ( ( non empty ) ( non empty ) set ) ) V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) BinOp of b1 : ( ( non empty ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [: the carrier of MidStr(# b1 : ( ( non empty ) ( non empty ) set ) ,(@ b3 : ( ( V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) : ( ( V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5(b1 : ( ( non empty ) ( non empty ) set ) ) V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) BinOp of b1 : ( ( non empty ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of MidStr(# b1 : ( ( non empty ) ( non empty ) set ) ,(@ b3 : ( ( V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) : ( ( V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) ( V1() V4([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5(b1 : ( ( non empty ) ( non empty ) set ) ) V6() V18([:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) BinOp of b1 : ( ( non empty ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) is associating ;

definition
let S be ( ( non empty ) ( non empty ) set ) ;
let G be ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) ;
let w be ( ( V6() V18([:S : ( ( non empty ) ( non empty ) set ) ,S : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of G : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([:S : ( ( non empty ) ( non empty ) set ) ,S : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of G : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([:S : ( ( non empty ) ( non empty ) set ) ,S : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of G : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [:S : ( ( non empty ) ( non empty ) set ) ,S : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of G : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ;
assume w : ( ( V6() V18([:S : ( ( non empty ) ( non empty ) set ) ,S : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of G : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([:S : ( ( non empty ) ( non empty ) set ) ,S : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of G : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([:S : ( ( non empty ) ( non empty ) set ) ,S : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of G : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [:S : ( ( non empty ) ( non empty ) set ) ,S : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of G : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) is_atlas_of S : ( ( non empty ) ( non empty ) set ) ,G : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) ;
func MidSp. w -> ( ( non empty strict MidSp-like ) ( non empty strict MidSp-like ) MidSp) equals :: MIDSP_2:def 11
 MidStr(# S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ,(@ w : ( ( V6() V18([:G : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) ) ) ( V1() V4([:G : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ) V5(G : ( ( ) ( ) set ) ) V6() V18([:G : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) ) ) Element of bool [:[:G : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( ( V6() V18([:S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ,S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) :] : ( ( ) ( ) set ) ,S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ) ( V1() V4([:S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ,S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) :] : ( ( ) ( ) set ) ) V5(S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) V6() V18([:S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ,S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) :] : ( ( ) ( ) set ) ,S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ) BinOp of S : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) #) : ( ( strict ) ( strict ) MidStr ) ;
end;

theorem :: MIDSP_2:27
for M being ( ( non empty ) ( non empty ) MidStr ) holds
( M : ( ( non empty ) ( non empty ) MidStr ) is ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) iff ex G being ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) ex w being ( ( V6() V18([: the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([: the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([: the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [: the carrier of M : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of M : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of G : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) st
( w : ( ( V6() V18([: the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([: the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([: the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [: the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) is_atlas_of the carrier of M : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) ,G : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) & w : ( ( V6() V18([: the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([: the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([: the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [: the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) is associating ) ) ;

definition
let M be ( ( non empty ) ( non empty ) MidStr ) ;
attr c2 is strict ;
struct AtlasStr over M -> ;
aggr AtlasStr(# algebra, function #) -> ( ( strict ) ( strict ) AtlasStr over M : ( ( non empty ) ( non empty ) MidStr ) ) ;
sel algebra c2 -> ( ( non empty ) ( non empty ) addLoopStr ) ;
sel function c2 -> ( ( V6() V18([: the carrier of M : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of M : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of the algebra of c2 : ( ( ) ( ) set ) : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([: the carrier of M : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of M : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of the algebra of c2 : ( ( ) ( ) set ) : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([: the carrier of M : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of M : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of the algebra of c2 : ( ( ) ( ) set ) : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [: the carrier of M : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of M : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of the algebra of c2 : ( ( ) ( ) set ) : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ;
end;

definition
let M be ( ( non empty ) ( non empty ) MidStr ) ;
let IT be ( ( ) ( ) AtlasStr over M : ( ( non empty ) ( non empty ) MidStr ) ) ;
attr IT is ATLAS-like means :: MIDSP_2:def 12
( the algebra of IT : ( ( ) ( ) set ) : ( ( non empty ) ( non empty ) addLoopStr ) is midpoint_operator & the algebra of IT : ( ( ) ( ) set ) : ( ( non empty ) ( non empty ) addLoopStr ) is add-associative & the algebra of IT : ( ( ) ( ) set ) : ( ( non empty ) ( non empty ) addLoopStr ) is right_zeroed & the algebra of IT : ( ( ) ( ) set ) : ( ( non empty ) ( non empty ) addLoopStr ) is right_complementable & the algebra of IT : ( ( ) ( ) set ) : ( ( non empty ) ( non empty ) addLoopStr ) is Abelian & the function of IT : ( ( ) ( ) set ) : ( ( V6() V18([: the carrier of M : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of M : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of the algebra of IT : ( ( ) ( ) set ) : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([: the carrier of M : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of M : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of the algebra of IT : ( ( ) ( ) set ) : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([: the carrier of M : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of M : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of the algebra of IT : ( ( ) ( ) set ) : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [: the carrier of M : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of M : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of the algebra of IT : ( ( ) ( ) set ) : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) is associating & the function of IT : ( ( ) ( ) set ) : ( ( V6() V18([: the carrier of M : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of M : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of the algebra of IT : ( ( ) ( ) set ) : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([: the carrier of M : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of M : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of the algebra of IT : ( ( ) ( ) set ) : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([: the carrier of M : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of M : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of the algebra of IT : ( ( ) ( ) set ) : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [: the carrier of M : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of M : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of the algebra of IT : ( ( ) ( ) set ) : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) is_atlas_of the carrier of M : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the algebra of IT : ( ( ) ( ) set ) : ( ( non empty ) ( non empty ) addLoopStr ) );
end;

registration
let M be ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ;
cluster ATLAS-like for ( ( ) ( ) AtlasStr over M : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidStr ) ) ;
end;

definition
let M be ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ;
mode ATLAS of M is ( ( ATLAS-like ) ( ATLAS-like ) AtlasStr over M : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidStr ) ) ;
end;

definition
let M be ( ( non empty ) ( non empty ) MidStr ) ;
let W be ( ( ) ( ) AtlasStr over M : ( ( non empty ) ( non empty ) MidStr ) ) ;
mode Vector of W is ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
end;

definition
let M be ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ;
let W be ( ( ) ( ) AtlasStr over M : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) ;
let a, b be ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ;
func W . (a,b) -> ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) equals :: MIDSP_2:def 13
 the function of W : ( ( ) ( ) set ) : ( ( V6() V18([: the carrier of M : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of M : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of the algebra of W : ( ( ) ( ) set ) : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([: the carrier of M : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of M : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of the algebra of W : ( ( ) ( ) set ) : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([: the carrier of M : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of M : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of the algebra of W : ( ( ) ( ) set ) : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [: the carrier of M : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of M : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of the algebra of W : ( ( ) ( ) set ) : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) . (a : ( ( V6() V18([:W : ( ( ) ( ) set ) ,W : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,W : ( ( ) ( ) set ) ) ) ( V1() V4([:W : ( ( ) ( ) set ) ,W : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ) V5(W : ( ( ) ( ) set ) ) V6() V18([:W : ( ( ) ( ) set ) ,W : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,W : ( ( ) ( ) set ) ) ) Element of bool [:[:W : ( ( ) ( ) set ) ,W : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,W : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of W : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of the carrier of the algebra of W : ( ( ) ( ) set ) : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ;
end;

definition
let M be ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ;
let W be ( ( ) ( ) AtlasStr over M : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) ;
let a be ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ;
let x be ( ( ) ( ) Vector of W : ( ( ) ( ) AtlasStr over M : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) ) ;
func (a,x) . W -> ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) equals :: MIDSP_2:def 14
(a : ( ( V6() V18([:W : ( ( ) ( ) set ) ,W : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,W : ( ( ) ( ) set ) ) ) ( V1() V4([:W : ( ( ) ( ) set ) ,W : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ) V5(W : ( ( ) ( ) set ) ) V6() V18([:W : ( ( ) ( ) set ) ,W : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,W : ( ( ) ( ) set ) ) ) Element of bool [:[:W : ( ( ) ( ) set ) ,W : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,W : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,x : ( ( ) ( ) Element of W : ( ( ) ( ) set ) ) ) . the function of W : ( ( ) ( ) set ) : ( ( V6() V18([: the carrier of M : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of M : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of the algebra of W : ( ( ) ( ) set ) : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([: the carrier of M : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of M : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of the algebra of W : ( ( ) ( ) set ) : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([: the carrier of M : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of M : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of the algebra of W : ( ( ) ( ) set ) : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [: the carrier of M : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of M : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of the algebra of W : ( ( ) ( ) set ) : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of M : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidStr ) : ( ( ) ( non empty ) set ) ) ;
end;

definition
let M be ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ;
let W be ( ( ATLAS-like ) ( ATLAS-like ) ATLAS of M : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) ;
func 0. W -> ( ( ) ( ) Vector of W : ( ( ) ( ) set ) ) equals :: MIDSP_2:def 15
 0. the algebra of W : ( ( ) ( ) set ) : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( V49( the algebra of W : ( ( ) ( ) set ) : ( ( non empty ) ( non empty ) addLoopStr ) ) ) Element of the carrier of the algebra of W : ( ( ) ( ) set ) : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ;
end;

theorem :: MIDSP_2:28
for G being ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr )
for M being ( ( non empty ) ( non empty ) MidStr )
for w being ( ( V6() V18([: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [: the carrier of M : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of M : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of G : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) )
for a, c, b1, b2 being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st w : ( ( V6() V18([: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) is_atlas_of the carrier of M : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) ,G : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) & w : ( ( V6() V18([: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) is associating holds
( a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) @ c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) ) = b1 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) @ b2 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) ) iff w : ( ( V6() V18([: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) . (a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) = (w : ( ( V6() V18([: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) . (a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b1 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) + (w : ( ( V6() V18([: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) . (a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b2 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: MIDSP_2:29
for G being ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr )
for M being ( ( non empty ) ( non empty ) MidStr )
for w being ( ( V6() V18([: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [: the carrier of M : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of M : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of G : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) )
for a, c, b being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st w : ( ( V6() V18([: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) is_atlas_of the carrier of M : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) ,G : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) & w : ( ( V6() V18([: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) is associating holds
( a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) @ c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) ) = b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) iff w : ( ( V6() V18([: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) . (a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) = Double (w : ( ( V6() V18([: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V1() V4([: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V5( the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) V6() V18([: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) Function of [: the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) MidStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) . (a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed midpoint_operator ) ( non empty right_complementable Fanoian Abelian add-associative right_zeroed midpoint_operator ) addLoopStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ;

theorem :: MIDSP_2:30
for M being ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp)
for W being ( ( ATLAS-like ) ( ATLAS-like ) ATLAS of M : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) )
for a, c, b1, b2 being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds
( a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) @ c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) : ( ( ) ( non empty ) set ) ) = b1 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) @ b2 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) : ( ( ) ( non empty ) set ) ) iff W : ( ( ATLAS-like ) ( ATLAS-like ) ATLAS of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) . (a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = (W : ( ( ATLAS-like ) ( ATLAS-like ) ATLAS of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) . (a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b1 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) + (W : ( ( ATLAS-like ) ( ATLAS-like ) ATLAS of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) . (a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b2 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of the algebra of b2 : ( ( ATLAS-like ) ( ATLAS-like ) ATLAS of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: MIDSP_2:31
for M being ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp)
for W being ( ( ATLAS-like ) ( ATLAS-like ) ATLAS of M : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) )
for a, c, b being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds
( a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) @ c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) : ( ( ) ( non empty ) set ) ) = b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) iff W : ( ( ATLAS-like ) ( ATLAS-like ) ATLAS of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) . (a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = Double (W : ( ( ATLAS-like ) ( ATLAS-like ) ATLAS of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) . (a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ;

theorem :: MIDSP_2:32
for M being ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp)
for W being ( ( ATLAS-like ) ( ATLAS-like ) ATLAS of M : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) holds
( ( for a being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for x being ( ( ) ( ) Vector of W : ( ( ATLAS-like ) ( ATLAS-like ) ATLAS of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) ) ex b being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st W : ( ( ATLAS-like ) ( ATLAS-like ) ATLAS of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) . (a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) & ( for a, b, c being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st W : ( ( ATLAS-like ) ( ATLAS-like ) ATLAS of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) . (a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = W : ( ( ATLAS-like ) ( ATLAS-like ) ATLAS of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) . (a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) = c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) & ( for a, b, c being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds (W : ( ( ATLAS-like ) ( ATLAS-like ) ATLAS of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) . (a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) + (W : ( ( ATLAS-like ) ( ATLAS-like ) ATLAS of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) . (b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of the algebra of b2 : ( ( ATLAS-like ) ( ATLAS-like ) ATLAS of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) = W : ( ( ATLAS-like ) ( ATLAS-like ) ATLAS of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) . (a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: MIDSP_2:33
for M being ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp)
for W being ( ( ATLAS-like ) ( ATLAS-like ) ATLAS of M : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) )
for a, b, c, d being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for x being ( ( ) ( ) Vector of W : ( ( ATLAS-like ) ( ATLAS-like ) ATLAS of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) ) holds
( W : ( ( ATLAS-like ) ( ATLAS-like ) ATLAS of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) . (a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = 0. W : ( ( ATLAS-like ) ( ATLAS-like ) ATLAS of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) : ( ( ) ( ) Vector of b2 : ( ( ATLAS-like ) ( ATLAS-like ) ATLAS of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) ) & ( W : ( ( ATLAS-like ) ( ATLAS-like ) ATLAS of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) . (a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = 0. W : ( ( ATLAS-like ) ( ATLAS-like ) ATLAS of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) : ( ( ) ( ) Vector of b2 : ( ( ATLAS-like ) ( ATLAS-like ) ATLAS of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) ) implies a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) = b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) & W : ( ( ATLAS-like ) ( ATLAS-like ) ATLAS of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) . (a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = - (W : ( ( ATLAS-like ) ( ATLAS-like ) ATLAS of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) . (b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of the algebra of b2 : ( ( ATLAS-like ) ( ATLAS-like ) ATLAS of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) & ( W : ( ( ATLAS-like ) ( ATLAS-like ) ATLAS of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) . (a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = W : ( ( ATLAS-like ) ( ATLAS-like ) ATLAS of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) . (c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,d : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) implies W : ( ( ATLAS-like ) ( ATLAS-like ) ATLAS of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) . (b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = W : ( ( ATLAS-like ) ( ATLAS-like ) ATLAS of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) . (d : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) & ( for b being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for x being ( ( ) ( ) Vector of W : ( ( ATLAS-like ) ( ATLAS-like ) ATLAS of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) ) ex a being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st W : ( ( ATLAS-like ) ( ATLAS-like ) ATLAS of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) . (a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) Vector of b2 : ( ( ATLAS-like ) ( ATLAS-like ) ATLAS of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) ) ) & ( W : ( ( ATLAS-like ) ( ATLAS-like ) ATLAS of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) . (b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = W : ( ( ATLAS-like ) ( ATLAS-like ) ATLAS of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) . (c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) implies b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) = c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) & ( a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) @ b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) : ( ( ) ( non empty ) set ) ) = c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) implies W : ( ( ATLAS-like ) ( ATLAS-like ) ATLAS of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) . (a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = W : ( ( ATLAS-like ) ( ATLAS-like ) ATLAS of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) . (c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) & ( W : ( ( ATLAS-like ) ( ATLAS-like ) ATLAS of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) . (a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = W : ( ( ATLAS-like ) ( ATLAS-like ) ATLAS of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) . (c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) implies a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) @ b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) : ( ( ) ( non empty ) set ) ) = c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) & ( a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) @ b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) : ( ( ) ( non empty ) set ) ) = c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) @ d : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) : ( ( ) ( non empty ) set ) ) implies W : ( ( ATLAS-like ) ( ATLAS-like ) ATLAS of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) . (a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,d : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = W : ( ( ATLAS-like ) ( ATLAS-like ) ATLAS of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) . (c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) & ( W : ( ( ATLAS-like ) ( ATLAS-like ) ATLAS of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) . (a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,d : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = W : ( ( ATLAS-like ) ( ATLAS-like ) ATLAS of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) . (c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) implies a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) @ b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) : ( ( ) ( non empty ) set ) ) = c : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) @ d : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) : ( ( ) ( non empty ) set ) ) ) & ( W : ( ( ATLAS-like ) ( ATLAS-like ) ATLAS of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) . (a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) Vector of b2 : ( ( ATLAS-like ) ( ATLAS-like ) ATLAS of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) ) implies (a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,x : ( ( ) ( ) Vector of b2 : ( ( ATLAS-like ) ( ATLAS-like ) ATLAS of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) ) ) . W : ( ( ATLAS-like ) ( ATLAS-like ) ATLAS of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) = b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) & ( (a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,x : ( ( ) ( ) Vector of b2 : ( ( ATLAS-like ) ( ATLAS-like ) ATLAS of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) ) ) . W : ( ( ATLAS-like ) ( ATLAS-like ) ATLAS of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) = b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) implies W : ( ( ATLAS-like ) ( ATLAS-like ) ATLAS of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) . (a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) Vector of b2 : ( ( ATLAS-like ) ( ATLAS-like ) ATLAS of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) ) ) ) ;

theorem :: MIDSP_2:34
for M being ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp)
for W being ( ( ATLAS-like ) ( ATLAS-like ) ATLAS of M : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) )
for a being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds (a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,(0. W : ( ( ATLAS-like ) ( ATLAS-like ) ATLAS of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) ) : ( ( ) ( ) Vector of b2 : ( ( ATLAS-like ) ( ATLAS-like ) ATLAS of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) ) ) . W : ( ( ATLAS-like ) ( ATLAS-like ) ATLAS of b1 : ( ( non empty MidSp-like ) ( non empty MidSp-like ) MidSp) ) : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) = a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ;