consider r9 being POINT of S such that
A3: between2 r,A,r9 by A1, A2, Th76;
set P = ((half-space3 (A,r)) \/ A) \/ (half-space3 (A,r9));
((half-space3 (A,r)) \/ A) \/ (half-space3 (A,r9)) is set ;
hence ex b₁ being Subset of S ex r9 being POINT of S st
( between2 r,A,r9 & b₁ = ((half-space3 (A,r)) \/ A) \/ (half-space3 (A,r9)) ) by A3; :: thesis: verum