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