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