( 2 is non zero Nat & |[0,0]| is Element of REAL 2 & |[1,1]| is Element of REAL 2 ) by EUCLID:22;
then consider S being ext-real-membered set such that
A1: S = { |.((|[0,0]| . i) - (|[1,1]| . i)).| where i is Element of Seg 2 : verum } and
A2: (Infty_dist 2) . (|[0,0]|,|[1,1]|) = sup S by Th57;
S = {|.(0 - 1).|}

proof

for t being object st t in S holds
t in {|.(0 - 1).|}

proof

let t be object ; :: thesis: ( t in S implies t in {|.(0 - 1).|} )
assume t in S ; :: thesis: t in {|.(0 - 1).|}
then consider i being Element of Seg 2 such that
A3: t = |.((|[0,0]| . i) - (|[1,1]| . i)).| by A1;

per cases ( i = 1 or i = 2 ) by FINSEQ_1:2, TARSKI:def 2;

suppose A4: i = 1 ; :: thesis: t in {|.(0 - 1).|}

thus t in {|.(0 - 1).|} by TARSKI:def 1, A4, A3; :: thesis: verum

end;

suppose A5: i = 2 ; :: thesis: t in {|.(0 - 1).|}

thus t in {|.(0 - 1).|} by TARSKI:def 1, A5, A3; :: thesis: verum

end;

end;

end;

then A6: S c= {|.(0 - 1).|} ;
{|.(0 - 1).|} c= S

proof

1 in Seg 2 ;
then |.((|[0,0]| . 1) - (|[1,1]| . 1)).| in S by A1;
hence {|.(0 - 1).|} c= S by TARSKI:def 1; :: thesis: verum

end;

hence S = {|.(0 - 1).|} by A6; :: thesis: verum

end;

then ( S = {|.(- 1).|} & |.(- 1).| = - (- 1) ) by ABSVALUE:def 1;
hence (Infty_dist 2) . (|[0,0]|,|[1,1]|) = 1 by A2, XXREAL_2:11; :: thesis: verum