set x = |[0,0]|;
set y = |[1,1]|;

now :: thesis: ex x, y being Element of the carrier of (TOP-REAL 2) st
( x in REAL 2 & y in REAL 2 & (Pitag_dist 2) . (x,y) <> (Infty_dist 2) . (x,y) )

take x = |[0,0]|; :: thesis: ex y being Element of the carrier of (TOP-REAL 2) st
( x in REAL 2 & y in REAL 2 & (Pitag_dist 2) . (x,y) <> (Infty_dist 2) . (x,y) )
take y = |[1,1]|; :: thesis: ( x in REAL 2 & y in REAL 2 & (Pitag_dist 2) . (x,y) <> (Infty_dist 2) . (x,y) )
( x is Element of REAL 2 & y is Element of REAL 2 ) by EUCLID:22;
hence ( x in REAL 2 & y in REAL 2 ) ; :: thesis: (Pitag_dist 2) . (x,y) <> (Infty_dist 2) . (x,y)
thus (Pitag_dist 2) . (x,y) <> (Infty_dist 2) . (x,y) by Th63, Th64, SQUARE_1:19; :: thesis: verum

end;

hence Pitag_dist 2 <> Infty_dist 2 ; :: thesis: verum