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 set ; :: 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 consider p being Point of (TOP-REAL 2) such that
A1: a = p and
p `1 < W-bound C ;
thus a in the carrier of (TOP-REAL 2) by A1; :: 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 ]|;
A2: (W-bound C) - 1 < (W-bound C) - 0 by XREAL_1:17;
|[((W-bound C) - 1),0 ]| `1 = (W-bound C) - 1 by EUCLID:56;
then A3: |[((W-bound C) - 1),0 ]| in A by A2;
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
A4: w1 = p and
A5: 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
A6: w2 = q and
A7: q `1 < W-bound C ;
let k be set ; :: according to TARSKI:def 3 :: thesis: ( not k in LSeg w1,w2 or k in A )
assume A8: 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;

suppose p `1 < q `1 ; :: thesis: k in A

then z `1 <= w2 `1 by A4, A6, A8, TOPREAL1:9;
then z `1 < W-bound C by A6, A7, XXREAL_0:2;
hence k in A ; :: thesis: verum

end;

suppose q `1 < p `1 ; :: thesis: k in A

then z `1 <= w1 `1 by A4, A6, A8, TOPREAL1:9;
then z `1 < W-bound C by A4, A5, XXREAL_0:2;
hence k in A ; :: thesis: verum

end;

suppose p `1 = q `1 ; :: thesis: k in A

then z `1 = p `1 by A4, A6, A8, GOBOARD7:5;
hence k in A by A5; :: thesis: verum

end;

end;

end;

then reconsider A = A as non empty convex Subset of (TOP-REAL 2) by A3;
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