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