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 ;
TARSKI:def 3 ( 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 }
;
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:]
;
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:]
; verum