let n be Nat; :: thesis: for A, B being Subset of (COMPLEX n) holds dist (A,B) = dist (B,A)
let A, B be Subset of (COMPLEX n); :: thesis: dist (A,B) = dist (B,A)
defpred S1[ set , set ] means ( $1 in B & $2 in A );
deffunc H1( Element of COMPLEX n, Element of COMPLEX n) -> Element of REAL = In (|.($1 - $2).|,REAL);
deffunc H2( Element of COMPLEX n, Element of COMPLEX n) -> Real = |.($1 - $2).|;
reconsider Y = { H1(z,z1) where z, z1 is Element of COMPLEX n : S1[z,z1] } as Subset of REAL from DOMAIN_1:sch 9();
 defpred S2[ set , set ] means ( $1 in A & $2 in B );
reconsider X = { H1(z1,z) where z1, z is Element of COMPLEX n : S2[z1,z] } as Subset of REAL from DOMAIN_1:sch 9();
A1: now :: thesis: for r being Element of REAL holds
( r in X iff r in Y )
let r be Element of REAL ; :: thesis: ( r in X iff r in Y )
A2: now :: thesis: ( ex z, z1 being Element of COMPLEX n st
( r = H1(z,z1) & z in B & z1 in A ) implies ex z1, z being Element of COMPLEX n st
( r = H1(z1,z) & z1 in A & z in B ) )
given z, z1 being Element of COMPLEX n such that A3: ( r = H1(z,z1) & z in B & z1 in A ) ; :: thesis: ex z1, z being Element of COMPLEX n st
( r = H1(z1,z) & z1 in A & z in B )
take z1 = z1; :: thesis: ex z being Element of COMPLEX n st
( r = H1(z1,z) & z1 in A & z in B )
take z = z; :: thesis: ( r = H1(z1,z) & z1 in A & z in B )
thus ( r = H1(z1,z) & z1 in A & z in B ) by A3, Th103; :: thesis: verum
end;
now :: thesis: ( ex z1, z being Element of COMPLEX n st
( r = H1(z1,z) & z1 in A & z in B ) implies ex z, z1 being Element of COMPLEX n st
( r = H1(z,z1) & z in B & z1 in A ) )
given z1, z being Element of COMPLEX n such that A4: ( r = H1(z1,z) & z1 in A & z in B ) ; :: thesis: ex z, z1 being Element of COMPLEX n st
( r = H1(z,z1) & z in B & z1 in A )
take z = z; :: thesis: ex z1 being Element of COMPLEX n st
( r = H1(z,z1) & z in B & z1 in A )
take z1 = z1; :: thesis: ( r = H1(z,z1) & z in B & z1 in A )
thus ( r = H1(z,z1) & z in B & z1 in A ) by A4, Th103; :: thesis: verum
end;
hence ( r in X iff r in Y ) by A2; :: thesis: verum
end;
A5: for z, z1 being Element of COMPLEX n holds H1(z,z1) = H2(z,z1) ;
A6: { H1(z,z1) where z, z1 is Element of COMPLEX n : S1[z,z1] } = { H2(z,z1) where z, z1 is Element of COMPLEX n : S1[z,z1] } from FRAENKEL:sch 7(A5);
 { H1(z1,z) where z1, z is Element of COMPLEX n : S2[z1,z] } = { H2(z1,z) where z1, z is Element of COMPLEX n : S2[z1,z] } from FRAENKEL:sch 7(A5);
 then ( dist (A,B) = lower_bound X & dist (B,A) = lower_bound Y ) by Def19, A6;
hence dist (A,B) = dist (B,A) by A1, SUBSET_1:3; :: thesis: verum