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
A3: 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
A4: 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 A3, A2;
hence r1 = r2 by A4, A2; :: thesis: verum