deffunc H₁( Element of COMPLEX n) -> Element of REAL = In (|.(x - $1).|,REAL);
deffunc H₂( Element of COMPLEX n) -> Real = |.(x - $1).|;
defpred S₁[ set ] means $1 in A;
reconsider X = { H₁(z) where z is Element of COMPLEX n : S₁[z] } as Subset of REAL from DOMAIN_1:sch 8();
A1: for z being Element of COMPLEX n holds H₁(z) = H₂(z) ;
A2: { H₁(z1) where z1 is Element of COMPLEX n : S₁[z1] } = { H₂(z2) where z2 is Element of COMPLEX n : S₁[z2] } from FRAENKEL:sch 5(A1);
take L = lower_bound X; :: thesis: for X being Subset of REAL st X = { |.(x - z).| where z is Element of COMPLEX n : z in A } holds
L = lower_bound X
thus for X being Subset of REAL st X = { |.(x - z).| where z is Element of COMPLEX n : z in A } holds
L = lower_bound X by A2; :: thesis: verum