let n be Nat; for A, B being Subset of (COMPLEX n) holds dist (A,B) = dist (B,A)
let A, B be Subset of (COMPLEX n); 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();
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; verum