:: deftheorem defines convex JORDAN1:def 1 :
for V being RealLinearSpace
for P being Subset of V holds
( P is convex iff for w1, w2 being Element of V st w1 in P & w2 in P holds
LSeg (w1,w2) c= P );