let S be IncSpace; 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; 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; ( 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
; 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; verum