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

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