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 )

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

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 :: thesis: ( not A on P implies ex B, C being POINT of S st

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

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

assume A2:
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

A3: {B,C,D} on P and

A4: not {B,C,D} is linear by Th41;

A5: B <> C by A4, Th15;

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 A3, ENUMSET1:3;

hence A6: {B,C} on P by Th9; :: thesis: not {A,B,C} is linear

assume {A,B,C} is linear ; :: thesis: contradiction

then consider K being LINE of S such that

A7: {A,B,C} on K ;

{B,C,A} on K by A7, ENUMSET1:59;

then A8: {B,C} \/ {A} on K by ENUMSET1:3;

then A9: A on K by Th8;

{B,C} on K by A8, Th10;

then K on P by A6, A5, Def14;

hence contradiction by A2, A9, Def17; :: thesis: verum

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

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

A3: {B,C,D} on P and

A4: not {B,C,D} is linear by Th41;

A5: B <> C by A4, Th15;

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 A3, ENUMSET1:3;

hence A6: {B,C} on P by Th9; :: thesis: not {A,B,C} is linear

assume {A,B,C} is linear ; :: thesis: contradiction

then consider K being LINE of S such that

A7: {A,B,C} on K ;

{B,C,A} on K by A7, ENUMSET1:59;

then A8: {B,C} \/ {A} on K by ENUMSET1:3;

then A9: A on K by Th8;

{B,C} on K by A8, Th10;

then K on P by A6, A5, Def14;

hence contradiction by A2, A9, Def17; :: thesis: verum

now :: thesis: ( A on P implies ex B, C being POINT of S st

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

hence
ex B, C being POINT of S st ( {B,C} on P & not {A,B,C} is linear ) )

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

A10: A <> B and

A11: B on P and

B on P by Def15;

consider C being POINT of S such that

A12: C on P and

A13: not {A,B,C} is linear by A10, Th44;

{B,C} on P by A11, A12, Th3;

hence ex B, C being POINT of S st

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

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

then consider B being POINT of S such that

A10: A <> B and

A11: B on P and

B on P by Def15;

consider C being POINT of S such that

A12: C on P and

A13: not {A,B,C} is linear by A10, Th44;

{B,C} on P by A11, A12, Th3;

hence ex B, C being POINT of S st

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

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