:: deftheorem defines setvect MIDSP_1:def 12 :
for M being MidSp holds setvect M = { X where X is Subset of [: the carrier of M, the carrier of M:] : X is Vector of M } ;