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
proof
assume x in setvect M ; :: thesis: x is Vector of M
then ex X being Subset of [: the carrier of M, the carrier of M:] st
( x = X & X is Vector of M ) ;
hence x is Vector of M ; :: thesis: verum
end;