:: deftheorem defines UMP JORDAN21:def 2 :
for P being Subset of the carrier of (TOP-REAL 2) holds UMP P = |[(((E-bound P) + (W-bound P)) / 2),(upper_bound (proj2 .: (P /\ (Vertical_Line (((E-bound P) + (W-bound P)) / 2)))))]|;