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 object ; :: 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 reconsider y = x as Point of (TOP-REAL 2) ;
A2: x in south_halfline p by A1, XBOOLE_0:def 5;
then A3: y `1 = p `1 by TOPREAL1:def 12;
then A4: x = |[(p `1),(y `2)]| by EUCLID:53;
A5: not x in {p} by A1, XBOOLE_0:def 5;
A6: now :: thesis: not y `2 = p `2
assume y `2 = p `2 ; :: thesis: contradiction
then x = p by A3, TOPREAL3:6;
hence contradiction by A5, TARSKI:def 1; :: thesis: verum
end;
y `2 <= p `2 by A2, TOPREAL1:def 12;
then y `2 < p `2 by A6, XXREAL_0:1;
hence x in { |[(p `1),r]| where r is Real : r < p `2 } by A4; :: thesis: verum
end;
let x be object ; :: 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
A7: x = |[(p `1),r]| and
A8: r < p `2 ;
reconsider y = x as Point of (TOP-REAL 2) by A7;
A9: y `2 = r by A7, EUCLID:52;
then A10: not x in {p} by A8, TARSKI:def 1;
y `1 = p `1 by A7, EUCLID:52;
then x in south_halfline p by A8, A9, TOPREAL1:def 12;
hence x in (south_halfline p) \ {p} by A10, XBOOLE_0:def 5; :: thesis: verum
end;
hence (south_halfline p) \ {p} is convex by Th5; :: thesis: verum