let a, b be real number ; ].a,b.] is convex Subset of R^1
reconsider P = ].a,b.] as Subset of R^1 by TOPMETR:24;
P is convex
proof
let x,
y be
Point of
R^1 ;
TOPALG_2:def 3 ( x in P & y in P implies [.x,y.] c= P )
assume
x in P
;
( not y in P or [.x,y.] c= P )
then A1:
a < x
by XXREAL_1:2;
assume
y in P
;
[.x,y.] c= P
then A2:
y <= b
by XXREAL_1:2;
let m be
set ;
TARSKI:def 3 ( not m in [.x,y.] or m in P )
assume A3:
m in [.x,y.]
;
m in P
then reconsider m =
m as
Real ;
x <= m
by A3, XXREAL_1:1;
then A4:
a < m
by A1, XXREAL_0:2;
m <= y
by A3, XXREAL_1:1;
then
m <= b
by A2, XXREAL_0:2;
hence
m in P
by A4, XXREAL_1:2;
verum
end;
hence
].a,b.] is convex Subset of R^1
; verum