let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( p1 `1 <> p2 `1 & p1 `2 <> p2 `2 implies ex p being Point of (TOP-REAL 2) st
( p in LSeg p1,p2 & p `1 <> p1 `1 & p `1 <> p2 `1 & p `2 <> p1 `2 & p `2 <> p2 `2 ) )
assume that
A1: p1 `1 <> p2 `1 and
A2: p1 `2 <> p2 `2 ; :: thesis: ex p being Point of (TOP-REAL 2) st
( p in LSeg p1,p2 & p `1 <> p1 `1 & p `1 <> p2 `1 & p `2 <> p1 `2 & p `2 <> p2 `2 )
take p = (1 / 2) * (p1 + p2); :: thesis: ( p in LSeg p1,p2 & p `1 <> p1 `1 & p `1 <> p2 `1 & p `2 <> p1 `2 & p `2 <> p2 `2 )
A3: p = ((1 - (1 / 2)) * p1) + ((1 / 2) * p2) by EUCLID:36;
hence p in LSeg p1,p2 ; :: thesis: ( p `1 <> p1 `1 & p `1 <> p2 `1 & p `2 <> p1 `2 & p `2 <> p2 `2 )

hereby :: thesis: ( p `1 <> p2 `1 & p `2 <> p1 `2 & p `2 <> p2 `2 )

assume A4: p `1 = p1 `1 ; :: thesis: contradiction
p `1 = (((1 - (1 / 2)) * p1) `1 ) + (((1 / 2) * p2) `1 ) by A3, TOPREAL3:7
.= ((1 - (1 / 2)) * (p1 `1 )) + (((1 / 2) * p2) `1 ) by TOPREAL3:9
.= ((1 - (1 / 2)) * (p `1 )) + ((1 / 2) * (p2 `1 )) by A4, TOPREAL3:9 ;
hence contradiction by A1, A4; :: thesis: verum

end;

hereby :: thesis: ( p `2 <> p1 `2 & p `2 <> p2 `2 )

assume A5: p `1 = p2 `1 ; :: thesis: contradiction
p `1 = (((1 - (1 / 2)) * p1) `1 ) + (((1 / 2) * p2) `1 ) by A3, TOPREAL3:7
.= ((1 - (1 / 2)) * (p1 `1 )) + (((1 / 2) * p2) `1 ) by TOPREAL3:9
.= ((1 - (1 / 2)) * (p1 `1 )) + ((1 / 2) * (p `1 )) by A5, TOPREAL3:9 ;
hence contradiction by A1, A5; :: thesis: verum

end;

hereby :: thesis: p `2 <> p2 `2

assume A6: p `2 = p1 `2 ; :: thesis: contradiction
p `2 = (((1 - (1 / 2)) * p1) `2 ) + (((1 / 2) * p2) `2 ) by A3, TOPREAL3:7
.= ((1 - (1 / 2)) * (p1 `2 )) + (((1 / 2) * p2) `2 ) by TOPREAL3:9
.= ((1 - (1 / 2)) * (p `2 )) + ((1 / 2) * (p2 `2 )) by A6, TOPREAL3:9 ;
hence contradiction by A2, A6; :: thesis: verum

end;

hereby :: thesis: verum

assume A7: p `2 = p2 `2 ; :: thesis: contradiction
p `2 = (((1 - (1 / 2)) * p1) `2 ) + (((1 / 2) * p2) `2 ) by A3, TOPREAL3:7
.= ((1 - (1 / 2)) * (p1 `2 )) + (((1 / 2) * p2) `2 ) by TOPREAL3:9
.= ((1 - (1 / 2)) * (p1 `2 )) + ((1 / 2) * (p `2 )) by A7, TOPREAL3:9 ;
hence contradiction by A2, A7; :: thesis: verum

end;