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

proof

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

let x be set ; :: thesis: ( x in (south_halfline p) \ {p} implies x in { |[(p `1 ),r]| where r is Real : r < p `2 } )
assume A1: x in (south_halfline p) \ {p} ; :: thesis: x in { |[(p `1 ),r]| where r is Real : r < p `2 }
then A2: x in south_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 14;

now

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

end;

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

end;

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

end;

hence (south_halfline p) \ {p} is convex by Th5; :: thesis: verum