let X, Y be Subset of S; ( ex r9 being POINT of S st
( between2 r,A,r9 & X = ((half-space3 (A,r)) \/ A) \/ (half-space3 (A,r9)) ) & ex r9 being POINT of S st
( between2 r,A,r9 & Y = ((half-space3 (A,r)) \/ A) \/ (half-space3 (A,r9)) ) implies X = Y )
assume that
A4:
ex r9 being POINT of S st
( between2 r,A,r9 & X = ((half-space3 (A,r)) \/ A) \/ (half-space3 (A,r9)) )
and
A5:
ex r9 being POINT of S st
( between2 r,A,r9 & Y = ((half-space3 (A,r)) \/ A) \/ (half-space3 (A,r9)) )
; X = Y
consider r9 being POINT of S such that
A6:
between2 r,A,r9
and
A7:
X = ((half-space3 (A,r)) \/ A) \/ (half-space3 (A,r9))
by A4;
consider r99 being POINT of S such that
A8:
between2 r,A,r99
and
A9:
Y = ((half-space3 (A,r)) \/ A) \/ (half-space3 (A,r99))
by A5;
A10:
half-space3 (A,r9) = { x where x is POINT of S : A out2 x,r9 }
by A6, Def18;
( between2 r9,A,r & between2 r99,A,r )
by A8, A6, GTARSKI3:14;
then
A out2 r99,r9
;
then
r99 in half-space3 (A,r9)
by A10;
hence
X = Y
by A6, A8, A7, A9, Th83; verum