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);
take L = lower_bound X; :: 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
L = lower_bound X
thus 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
L = lower_bound X by A2; :: thesis: verum