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