defpred S₁[ set ] means $1 in A;
deffunc H₁( Element of COMPLEX n) -> Real = |.(x - $1).|;
reconsider X = { H₁(z) where z is Element of COMPLEX n : S₁[z] } as Subset of REAL from COMPLSP1:sch 1();
take 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
lower_bound X = 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
lower_bound X = lower_bound X ; :: thesis: verum