let P be Subset of R^1 ; :: thesis: ( P is empty implies P is convex )
assume A1: P is empty ; :: thesis: P is convex
let a, b be Point of R^1 ; :: according to TOPALG_2:def 3 :: thesis: ( a in P & b in P implies [.a,b.] c= P )
thus ( a in P & b in P implies [.a,b.] c= P ) by A1; :: thesis: verum