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