take lower_bound X ; :: thesis: for X being Subset of REAL st X = { |.(x - z).| where x, z is Element of COMPLEX n : ( x in A & z in B ) } holds
lower_bound X = lower_bound X
thus for X being Subset of REAL st X = { |.(x - z).| where x, z is Element of COMPLEX n : ( x in A & z in B ) } holds
lower_bound X = lower_bound X by A2; :: thesis: verum