:: deftheorem Def1 defines x_Middle JORDAN6:def 1 :
for P being Subset of (TOP-REAL 2)
for p1, p2, b₄ being Point of (TOP-REAL 2) holds
( b₄ = x_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 `1 = ((p1 `1) + (p2 `1)) / 2 } holds
b₄ = First_Point (P,p1,p2,Q) );