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 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

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, Th121; :: 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, Th121; :: 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 Def22;
hence dist (A,B) = dist (B,A) by A1, SUBSET_1:3; :: thesis: verum