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 by A2; :: thesis: verum