let n be Element of NAT ; :: thesis: for a, b being Point of (TOP-REAL n) holds LSeg a,b is convex
let a, b be Point of (TOP-REAL n); :: thesis: LSeg a,b is convex
set A = LSeg a,b;
let w1, w2 be Point of (TOP-REAL n); :: according to JORDAN1:def 1 :: thesis: ( not w1 in LSeg a,b or not w2 in LSeg a,b or LSeg w1,w2 c= LSeg a,b )
assume ( w1 in LSeg a,b & w2 in LSeg a,b ) ; :: thesis: LSeg w1,w2 c= LSeg a,b
hence LSeg w1,w2 c= LSeg a,b by TOPREAL1:12; :: thesis: verum