let C be Subset of (TOP-REAL 2); :: thesis: { p where p is Point of (TOP-REAL 2) : p `1 < W-bound C } is non empty connected convex Subset of (TOP-REAL 2)
set A = { p where p is Point of (TOP-REAL 2) : p `1 < W-bound C } ;
{ p where p is Point of (TOP-REAL 2) : p `1 < W-bound C } c= the carrier of (TOP-REAL 2)
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { p where p is Point of (TOP-REAL 2) : p `1 < W-bound C } or a in the carrier of (TOP-REAL 2) )
assume a in { p where p is Point of (TOP-REAL 2) : p `1 < W-bound C } ; :: thesis: a in the carrier of (TOP-REAL 2)
then ex p being Point of (TOP-REAL 2) st
( a = p & p `1 < W-bound C ) ;
hence a in the carrier of (TOP-REAL 2) ; :: thesis: verum
end;
then reconsider A = { p where p is Point of (TOP-REAL 2) : p `1 < W-bound C } as Subset of (TOP-REAL 2) ;
set p = W-bound C;
set b = |[((W-bound C) - 1),0]|;
A1: |[((W-bound C) - 1),0]| `1 = (W-bound C) - 1 ;
(W-bound C) - 1 < (W-bound C) - 0 by XREAL_1:15;
then A2: |[((W-bound C) - 1),0]| in A by A1;
A is convex
proof
let w1, w2 be Point of (TOP-REAL 2); :: according to JORDAN1:def 1 :: thesis: ( not w1 in A or not w2 in A or LSeg (w1,w2) c= A )
assume w1 in A ; :: thesis: ( not w2 in A or LSeg (w1,w2) c= A )
then consider p being Point of (TOP-REAL 2) such that
A3: w1 = p and
A4: p `1 < W-bound C ;
assume w2 in A ; :: thesis: LSeg (w1,w2) c= A
then consider q being Point of (TOP-REAL 2) such that
A5: w2 = q and
A6: q `1 < W-bound C ;
let k be object ; :: according to TARSKI:def 3 :: thesis: ( not k in LSeg (w1,w2) or k in A )
assume A7: k in LSeg (w1,w2) ; :: thesis: k in A
then reconsider z = k as Point of (TOP-REAL 2) ;
per cases ( p `1 < q `1 or q `1 < p `1 or p `1 = q `1 ) by XXREAL_0:1;
end;
end;
then reconsider A = A as non empty convex Subset of (TOP-REAL 2) by A2;
A is connected ;
hence { p where p is Point of (TOP-REAL 2) : p `1 < W-bound C } is non empty connected convex Subset of (TOP-REAL 2) ; :: thesis: verum