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
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();
( r1 = lower_bound X & r2 = lower_bound X ) by A1, A2;
hence r1 = r2 ; :: thesis: verum