let n be Nat; :: thesis: for p, q being Point of (TOP-REAL n) st p = (1 / 2) * (p + q) holds

p = q

let p, q be Point of (TOP-REAL n); :: thesis: ( p = (1 / 2) * (p + q) implies p = q )

assume p = (1 / 2) * (p + q) ; :: thesis: p = q

then p = ((1 - (1 / 2)) * p) + ((1 / 2) * q) by RLVECT_1:def 5;

hence p = q by Th3; :: thesis: verum

p = q

let p, q be Point of (TOP-REAL n); :: thesis: ( p = (1 / 2) * (p + q) implies p = q )

assume p = (1 / 2) * (p + q) ; :: thesis: p = q

then p = ((1 - (1 / 2)) * p) + ((1 / 2) * q) by RLVECT_1:def 5;

hence p = q by Th3; :: thesis: verum