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

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 Th71;
A5: B <> C by A4, Th36;
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:43;
hence A6: {B,C} on P by Th19; :: 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 by Def6;
{B,C,A} on K by A7, ENUMSET1:100;
then A8: {B,C} \/ {A} on K by ENUMSET1:43;
then A9: A on K by Th18;
{B,C} on K by A8, Th20;
then K on P by A6, A5, Def14;
hence contradiction by A2, A9, Def17; :: thesis: verum

end;

now

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, Th74;
{B,C} on P by A11, A12, Th13;
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