let L be non empty addLoopStr ; :: thesis: ( L is midpoint_operator implies L is Fanoian )
assume A1: L is midpoint_operator ; :: thesis: L is Fanoian
let a be Element of L; :: according to VECTSP_1:def 17 :: thesis: ( not a + a = 0. L or a = 0. L )
assume a + a = 0. L ; :: thesis: a = 0. L
then Double a = 0. L ;
hence a = 0. L by A1; :: thesis: verum