let M be MidSp; :: thesis: for x being set holds

( x is Vector of M iff x in setvect M )

let x be set ; :: thesis: ( x is Vector of M iff x in setvect M )

thus ( x is Vector of M implies x in setvect M ) ; :: thesis: ( x in setvect M implies x is Vector of M )

thus ( x in setvect M implies x is Vector of M ) :: thesis: verum

( x is Vector of M iff x in setvect M )

let x be set ; :: thesis: ( x is Vector of M iff x in setvect M )

thus ( x is Vector of M implies x in setvect M ) ; :: thesis: ( x in setvect M implies x is Vector of M )

thus ( x in setvect M implies x is Vector of M ) :: thesis: verum