let p be Point of (TOP-REAL 2); :: thesis: (west_halfline p) \ {p} is convex
set P = (west_halfline p) \ {p};
(west_halfline p) \ {p} = { |[r,(p `2 )]| where r is Real : r < p `1 }

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: { |[r,(p `2 )]| where r is Real : r < p `1 } c= (west_halfline p) \ {p}

let x be set ; :: thesis: ( x in (west_halfline p) \ {p} implies x in { |[r,(p `2 )]| where r is Real : r < p `1 } )
assume A1: x in (west_halfline p) \ {p} ; :: thesis: x in { |[r,(p `2 )]| where r is Real : r < p `1 }
then A2: x in west_halfline p by XBOOLE_0:def 5;
A3: not x in {p} by A1, XBOOLE_0:def 5;
reconsider y = x as Point of (TOP-REAL 2) by A1;
A4: ( y `1 <= p `1 & y `2 = p `2 ) by A2, TOPREAL1:def 15;

now

assume y `1 = p `1 ; :: thesis: contradiction
then x = p by A4, TOPREAL3:11;
hence contradiction by A3, TARSKI:def 1; :: thesis: verum

end;

then A5: y `1 < p `1 by A4, XXREAL_0:1;
x = |[(y `1 ),(p `2 )]| by A4, EUCLID:57;
hence x in { |[r,(p `2 )]| where r is Real : r < p `1 } by A5; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { |[r,(p `2 )]| where r is Real : r < p `1 } or x in (west_halfline p) \ {p} )
assume x in { |[r,(p `2 )]| where r is Real : r < p `1 } ; :: thesis: x in (west_halfline p) \ {p}
then consider r being Real such that
A6: x = |[r,(p `2 )]| and
A7: r < p `1 ;
reconsider y = x as Point of (TOP-REAL 2) by A6;
A8: ( y `1 = r & y `2 = p `2 ) by A6, EUCLID:56;
then A9: x in west_halfline p by A7, TOPREAL1:def 15;
not x in {p} by A7, A8, TARSKI:def 1;
hence x in (west_halfline p) \ {p} by A9, XBOOLE_0:def 5; :: thesis: verum

end;

hence (west_halfline p) \ {p} is convex by Th3; :: thesis: verum