consider r being POINT of S such that
A5: not r in A and
A6: r in A9 by A1, A2, A3, Th38;
set P = Plane (A,r);
take Plane (A,r) ; :: thesis: ex r being POINT of S st
( not r in A & r in A9 & Plane (A,r) = Plane (A,r) )
thus ex r being POINT of S st
( not r in A & r in A9 & Plane (A,r) = Plane (A,r) ) by A5, A6; :: thesis: verum