:: deftheorem Def2 defines y_Middle JORDAN6:def 2 :
for P being Subset of (TOP-REAL 2)
for p1, p2, b₄ being Point of (TOP-REAL 2) holds
( b₄ = y_Middle (P,p1,p2) iff for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } holds
b₄ = First_Point (P,p1,p2,Q) );