set S = { [x,y] where x, y is Element of MS : dist (x,y) <= r } ;
{ [x,y] where x, y is Element of MS : dist (x,y) <= r } c= [: the carrier of MS, the carrier of MS:]

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in { [x,y] where x, y is Element of MS : dist (x,y) <= r } or t in [: the carrier of MS, the carrier of MS:] )
assume t in { [x,y] where x, y is Element of MS : dist (x,y) <= r } ; :: thesis: t in [: the carrier of MS, the carrier of MS:]
then ex x, y being Element of MS st
( t = [x,y] & dist (x,y) <= r ) ;
hence t in [: the carrier of MS, the carrier of MS:] ; :: thesis: verum

end;

hence { [x,y] where x, y is Element of MS : dist (x,y) <= r } is Subset of [: the carrier of MS, the carrier of MS:] ; :: thesis: verum