set M = Tarski0Space ;

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

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

proof

hence
Tarski0Space is close-everywhere
; :: thesis: verum
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;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