let S be IncSpace; :: thesis: for A being POINT of S
for P being PLANE of S ex B, C being POINT of S st
( {B,C} on P & not {A,B,C} is linear )
let A be POINT of S; :: thesis: for P being PLANE of S ex B, C being POINT of S st
( {B,C} on P & not {A,B,C} is linear )
let P be PLANE of S; :: thesis: ex B, C being POINT of S st
( {B,C} on P & not {A,B,C} is linear )

A1: now :: thesis: ( not A on P implies ex B, C being POINT of S st
( {B,C} on P & not {A,B,C} is linear ) )

assume A2: not A on P ; :: thesis: ex B, C being POINT of S st
( {B,C} on P & not {A,B,C} is linear )
consider B, C, D being POINT of S such that
A3: {B,C,D} on P and
A4: not {B,C,D} is linear by Th41;
A5: B <> C by A4, Th15;
take B = B; :: thesis: ex C being POINT of S st
( {B,C} on P & not {A,B,C} is linear )
take C = C; :: thesis: ( {B,C} on P & not {A,B,C} is linear )
{B,C} \/ {D} on P by A3, ENUMSET1:3;
hence A6: {B,C} on P by Th9; :: thesis: not {A,B,C} is linear
assume {A,B,C} is linear ; :: thesis: contradiction
then consider K being LINE of S such that
A7: {A,B,C} on K ;
{B,C,A} on K by A7, ENUMSET1:59;
then A8: {B,C} \/ {A} on K by ENUMSET1:3;
then A9: A on K by Th8;
{B,C} on K by A8, Th10;
then K on P by A6, A5, Def14;
hence contradiction by A2, A9, Def17; :: thesis: verum

end;

now :: thesis: ( A on P implies ex B, C being POINT of S st
( {B,C} on P & not {A,B,C} is linear ) )

assume A on P ; :: thesis: ex B, C being POINT of S st
( {B,C} on P & not {A,B,C} is linear )
then consider B being POINT of S such that
A10: A <> B and
A11: B on P and
B on P by Def15;
consider C being POINT of S such that
A12: C on P and
A13: not {A,B,C} is linear by A10, Th44;
{B,C} on P by A11, A12, Th3;
hence ex B, C being POINT of S st
( {B,C} on P & not {A,B,C} is linear ) by A13; :: thesis: verum

end;

hence ex B, C being POINT of S st
( {B,C} on P & not {A,B,C} is linear ) by A1; :: thesis: verum