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
A3: 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
A4: 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
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).|;
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();
A1: for z1, z2 being Element of COMPLEX n holds H₁(z1,z2) = H₂(z1,z2) ;
A2: { H₁(z1,z2) where z1, z2 is Element of COMPLEX n : S₁[z1,z2] } = { H₂(z1,z2) where z1, z2 is Element of COMPLEX n : S₁[z1,z2] } from FRAENKEL:sch 7(A1);
r1 = lower_bound X by A3, A2;
hence r1 = r2 by A4, A2; :: thesis: verum