let X, Y be Subset of S; :: thesis: ( ex r9 being POINT of S st
( between r,A,r9 & X = ((half-plane (A,r)) \/ A) \/ (half-plane (A,r9)) ) & ex r9 being POINT of S st
( between r,A,r9 & Y = ((half-plane (A,r)) \/ A) \/ (half-plane (A,r9)) ) implies X = Y )
assume that
A4: ex r9 being POINT of S st
( between r,A,r9 & X = ((half-plane (A,r)) \/ A) \/ (half-plane (A,r9)) ) and
A5: ex r9 being POINT of S st
( between r,A,r9 & Y = ((half-plane (A,r)) \/ A) \/ (half-plane (A,r9)) ) ; :: thesis: X = Y
consider r9 being POINT of S such that
A6: between r,A,r9 and
A7: X = ((half-plane (A,r)) \/ A) \/ (half-plane (A,r9)) by A4;
consider r99 being POINT of S such that
A8: between r,A,r99 and
A9: Y = ((half-plane (A,r)) \/ A) \/ (half-plane (A,r99)) by A5;
( between r9,A,r & between r99,A,r ) by A8, A6, GTARSKI3:14;
then A out r99,r9 ;
then r99 in half-plane (A,r9) ;
hence X = Y by A7, A9, A6, A8, Th23; :: thesis: verum