let n be Element of 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 EUCLID:32;
hence p = q by Th13; :: thesis: verum