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();
let r1, r2 be Real; :: thesis: ( ( for X being Subset of REAL st X = { |.(x - z).| where z is Element of COMPLEX n : z in A } holds
r1 = lower_bound X ) & ( for X being Subset of REAL st X = { |.(x - z).| where z is Element of COMPLEX n : z in A } holds
r2 = lower_bound X ) implies r1 = r2 )
assume that
A1: for X being Subset of REAL st X = { |.(x - z).| where z is Element of COMPLEX n : z in A } holds
r1 = lower_bound X and
A2: for X being Subset of REAL st X = { |.(x - z).| where z is Element of COMPLEX n : z in A } holds
r2 = lower_bound X ; :: thesis: r1 = r2
r1 = lower_bound X by A1;
hence r1 = r2 by A2; :: thesis: verum