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 ) )
assume A1: A <> B ; :: thesis: ex C being POINT of S st
( C on P & not {A,B,C} is linear )
consider L being LINE of S such that
A2: {A,B} on L by Def9;
consider C, D, E being POINT of S such that
A3: {C,D,E} on P and
A4: not {C,D,E} is linear by Th71;
not {C,D,E} on L by A4, Def6;
then ( not C on L or not D on L or not E on L ) by Th12;
then ( ( not {A,B,C} is linear or not {A,B,D} is linear or not {A,B,E} is linear ) & C on P & D on P & E on P ) by A1, A2, A3, Th14, Th39;
hence ex C being POINT of S st
( C on P & not {A,B,C} is linear ) ; :: thesis: verum