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