let S be IncSpace; :: thesis: for A, B being POINT of S

for P being PLANE of S st A <> B holds

ex C being POINT of S st

( C on P & not {A,B,C} is linear )

let A, B be POINT of S; :: thesis: for P being PLANE of S st A <> B holds

ex C being POINT of S st

( C on P & not {A,B,C} is linear )

let P be PLANE of S; :: thesis: ( A <> B implies ex C being POINT of S st

( C on P & not {A,B,C} is linear ) )

consider L being LINE of S such that

A1: {A,B} on L by Def9;

consider C, D, E being POINT of S such that

A2: {C,D,E} on P and

A3: not {C,D,E} is linear by Th41;

A4: ( C on P & D on P ) by A2, Th4;

not {C,D,E} on L by A3;

then A5: ( not C on L or not D on L or not E on L ) by Th2;

A6: E on P by A2, Th4;

assume A <> B ; :: thesis: ex C being POINT of S st

( C on P & not {A,B,C} is linear )

then ( not {A,B,C} is linear or not {A,B,D} is linear or not {A,B,E} is linear ) by A1, A5, Th18;

hence ex C being POINT of S st

( C on P & not {A,B,C} is linear ) by A4, A6; :: thesis: verum

for P being PLANE of S st A <> B holds

ex C being POINT of S st

( C on P & not {A,B,C} is linear )

let A, B be POINT of S; :: thesis: for P being PLANE of S st A <> B holds

ex C being POINT of S st

( C on P & not {A,B,C} is linear )

let P be PLANE of S; :: thesis: ( A <> B implies ex C being POINT of S st

( C on P & not {A,B,C} is linear ) )

consider L being LINE of S such that

A1: {A,B} on L by Def9;

consider C, D, E being POINT of S such that

A2: {C,D,E} on P and

A3: not {C,D,E} is linear by Th41;

A4: ( C on P & D on P ) by A2, Th4;

not {C,D,E} on L by A3;

then A5: ( not C on L or not D on L or not E on L ) by Th2;

A6: E on P by A2, Th4;

assume A <> B ; :: thesis: ex C being POINT of S st

( C on P & not {A,B,C} is linear )

then ( not {A,B,C} is linear or not {A,B,D} is linear or not {A,B,E} is linear ) by A1, A5, Th18;

hence ex C being POINT of S st

( C on P & not {A,B,C} is linear ) by A4, A6; :: thesis: verum