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
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 A2:
A <> B
and A3:
(
B on P &
B on P )
by Def15;
consider C being
POINT of
S such that A4:
C on P
and A5:
not
{A,B,C} is
linear
by A2, Th74;
{B,C} on P
by A3, A4, Th13;
hence
ex
B,
C being
POINT of
S st
(
{B,C} on P & not
{A,B,C} is
linear )
by A5;
:: thesis: verum end;
now assume A6:
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 A7:
{B,C,D} on P
and A8:
not
{B,C,D} is
linear
by Th71;
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 A7, ENUMSET1:43;
hence A9:
{B,C} on P
by Th19;
:: thesis: not {A,B,C} is linearassume
{A,B,C} is
linear
;
:: thesis: contradictionthen consider K being
LINE of
S such that A10:
{A,B,C} on K
by Def6;
{B,C,A} on K
by A10, ENUMSET1:100;
then A11:
{B,C} \/ {A} on K
by ENUMSET1:43;
then
(
B <> C &
{B,C} on K )
by A8, Th20, Th36;
then
(
K on P &
A on K )
by A9, A11, Def14, Th18;
hence
contradiction
by A6, Def17;
:: 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