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 S₁[ set , set ] means ( $1 in B & $2 in A );
deffunc H₁( Element of COMPLEX n, Element of COMPLEX n) -> Element of REAL = In (|.($1 - $2).|,REAL);
deffunc H₂( Element of COMPLEX n, Element of COMPLEX n) -> Real = |.($1 - $2).|;
reconsider Y = { H₁(z,z1) where z, z1 is Element of COMPLEX n : S₁[z,z1] } as Subset of REAL from DOMAIN_1:sch 9();
defpred S₂[ set , set ] means ( $1 in A & $2 in B );
reconsider X = { H₁(z1,z) where z1, z is Element of COMPLEX n : S₂[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 = H₁(z,z1) & z in B & z1 in A ) implies ex z1, z being Element of COMPLEX n st
( r = H₁(z1,z) & z1 in A & z in B ) )

given z, z1 being Element of COMPLEX n such that A3: ( r = H₁(z,z1) & z in B & z1 in A ) ; :: thesis: ex z1, z being Element of COMPLEX n st
( r = H₁(z1,z) & z1 in A & z in B )
take z1 = z1; :: thesis: ex z being Element of COMPLEX n st
( r = H₁(z1,z) & z1 in A & z in B )
take z = z; :: thesis: ( r = H₁(z1,z) & z1 in A & z in B )
thus ( r = H₁(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 = H₁(z1,z) & z1 in A & z in B ) implies ex z, z1 being Element of COMPLEX n st
( r = H₁(z,z1) & z in B & z1 in A ) )

given z1, z being Element of COMPLEX n such that A4: ( r = H₁(z1,z) & z1 in A & z in B ) ; :: thesis: ex z, z1 being Element of COMPLEX n st
( r = H₁(z,z1) & z in B & z1 in A )
take z = z; :: thesis: ex z1 being Element of COMPLEX n st
( r = H₁(z,z1) & z in B & z1 in A )
take z1 = z1; :: thesis: ( r = H₁(z,z1) & z in B & z1 in A )
thus ( r = H₁(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 H₁(z,z1) = H₂(z,z1) ;
A6: { H₁(z,z1) where z, z1 is Element of COMPLEX n : S₁[z,z1] } = { H₂(z,z1) where z, z1 is Element of COMPLEX n : S₁[z,z1] } from FRAENKEL:sch 7(A5);
{ H₁(z1,z) where z1, z is Element of COMPLEX n : S₂[z1,z] } = { H₂(z1,z) where z1, z is Element of COMPLEX n : S₂[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