let p be Point of (TOP-REAL 2); :: thesis: (east_halfline p) \ {p} is convex
set P = (east_halfline p) \ {p};
(east_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= (east_halfline p) \ {p}

let x be object ; :: thesis: ( x in (east_halfline p) \ {p} implies x in { |[r,(p `2)]| where r is Real : r > p `1 } )
assume A1: x in (east_halfline p) \ {p} ; :: thesis: x in { |[r,(p `2)]| where r is Real : r > p `1 }
then reconsider y = x as Point of (TOP-REAL 2) ;
A2: x in east_halfline p by A1, XBOOLE_0:def 5;
then A3: y `2 = p `2 by TOPREAL1:def 11;
then A4: x = |[(y `1),(p `2)]| by EUCLID:53;
A5: not x in {p} by A1, XBOOLE_0:def 5;

A6: now :: thesis: not y `1 = p `1

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

end;

y `1 >= p `1 by A2, TOPREAL1:def 11;
then y `1 > p `1 by A6, XXREAL_0:1;
hence x in { |[r,(p `2)]| where r is Real : r > p `1 } by A4; :: thesis: verum

end;

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

end;

hence (east_halfline p) \ {p} is convex by Th2; :: thesis: verum