set M = Tarski0Space ;
for a, b being Element of Tarski0Space holds dist (a,b) = 0

proof

let a, b be Element of Tarski0Space; :: thesis: dist (a,b) = 0
aa: MetrStruct(# the carrier of Tarski0Space, the distance of Tarski0Space #) = MetrStruct(# the carrier of ZeroSpace, the distance of ZeroSpace #) by TADef;
reconsider a1 = a, b1 = b as Element of 2 by aa;
thus dist (a,b) = 0 by METRIC_1:27, aa; :: thesis: verum

end;

hence Tarski0Space is close-everywhere ; :: thesis: verum