( 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;
end;
then A6: S c= {|.(0 - 1).|} ;
{|.(0 - 1).|} c= S
proof
A7: ( |[0,0]| . 1 = 0 & |[1,1]| . 1 = 1 ) by FINSEQ_1:44;
1 in Seg 2 ;
then |.((|[0,0]| . 1) - (|[1,1]| . 1)).| in S by A1;
hence {|.(0 - 1).|} c= S by A7, 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