let n be Element of 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) -> Real = |.($1 - $2).|;
reconsider Y = { H₁(z,z1) where z, z1 is Element of COMPLEX n : S₁[z,z1] } as Subset of REAL from COMPLSP1:sch 2();
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 COMPLSP1:sch 2();

A1: now

let r be Real; :: thesis: ( r in X iff r in Y )

A2: now

given z, z1 being Element of COMPLEX n such that A3: ( r = |.(z - z1).| & z in B & z1 in A ) ; :: thesis: ex z1, z being Element of COMPLEX n st
( r = |.(z1 - z).| & z1 in A & z in B )
take z1 = z1; :: thesis: ex z being Element of COMPLEX n st
( r = |.(z1 - z).| & z1 in A & z in B )
take z = z; :: thesis: ( r = |.(z1 - z).| & z1 in A & z in B )
thus ( r = |.(z1 - z).| & z1 in A & z in B ) by A3, Th74; :: thesis: verum

end;

now

given z1, z being Element of COMPLEX n such that A4: ( r = |.(z1 - z).| & z1 in A & z in B ) ; :: thesis: ex z, z1 being Element of COMPLEX n st
( r = |.(z - z1).| & z in B & z1 in A )
take z = z; :: thesis: ex z1 being Element of COMPLEX n st
( r = |.(z - z1).| & z in B & z1 in A )
take z1 = z1; :: thesis: ( r = |.(z - z1).| & z in B & z1 in A )
thus ( r = |.(z - z1).| & z in B & z1 in A ) by A4, Th74; :: thesis: verum

end;

hence ( r in X iff r in Y ) by A2; :: thesis: verum

end;

( dist A,B = lower_bound X & dist B,A = lower_bound Y ) by Def20;
hence dist A,B = dist B,A by A1, SUBSET_1:8; :: thesis: verum