deffunc H₁( Element of COMPLEX n, Element of COMPLEX n) -> Real = |.($1 - $2).|;
defpred S₁[ set , set ] means ( $1 in A & $2 in B );
reconsider X = { H₁(x,z) where x, z is Element of COMPLEX n : S₁[x,z] } as Subset of REAL from DOMAIN_1:sch 9();
let r1, r2 be Real; :: thesis: ( ( for X being Subset of REAL st X = { |.(x - z).| where x, z is Element of COMPLEX n : ( x in A & z in B ) } holds
r1 = lower_bound X ) & ( for X being Subset of REAL st X = { |.(x - z).| where x, z is Element of COMPLEX n : ( x in A & z in B ) } holds
r2 = lower_bound X ) implies r1 = r2 )
assume that
A1: for X being Subset of REAL st X = { |.(x - z).| where x, z is Element of COMPLEX n : ( x in A & z in B ) } holds
r1 = lower_bound X and
A2: for X being Subset of REAL st X = { |.(x - z).| where x, z is Element of COMPLEX n : ( x in A & z in B ) } holds
r2 = lower_bound X ; :: thesis: r1 = r2
r1 = lower_bound X by A1;
hence r1 = r2 by A2; :: thesis: verum