let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( p1 `2 < p2 `2 implies ((1 / 2) * (p1 + p2)) `2 < p2 `2 )
assume A1: p1 `2 < p2 `2 ; :: thesis: ((1 / 2) * (p1 + p2)) `2 < p2 `2
((1 / 2) * (p1 + p2)) `2 = (1 / 2) * ((p1 + p2) `2) by TOPREAL3:4
.= (1 / 2) * ((p1 `2) + (p2 `2)) by TOPREAL3:2
.= ((p1 `2) + (p2 `2)) / 2 ;
hence ((1 / 2) * (p1 + p2)) `2 < p2 `2 by A1, XREAL_1:226; :: thesis: verum