let S be IncSpace; :: thesis: for A, B being POINT of S st A <> B holds

ex C, D being POINT of S st not {A,B,C,D} is planar

let A, B be POINT of S; :: thesis: ( A <> B implies ex C, D being POINT of S st not {A,B,C,D} is planar )

set P = the PLANE of S;

assume A <> B ; :: thesis: not for C, D being POINT of S holds {A,B,C,D} is planar

then consider C being POINT of S such that

C on the PLANE of S and

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

not for D being POINT of S holds {A,B,C,D} is planar by A1, Th45;

hence not for C, D being POINT of S holds {A,B,C,D} is planar ; :: thesis: verum

ex C, D being POINT of S st not {A,B,C,D} is planar

let A, B be POINT of S; :: thesis: ( A <> B implies ex C, D being POINT of S st not {A,B,C,D} is planar )

set P = the PLANE of S;

assume A <> B ; :: thesis: not for C, D being POINT of S holds {A,B,C,D} is planar

then consider C being POINT of S such that

C on the PLANE of S and

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

not for D being POINT of S holds {A,B,C,D} is planar by A1, Th45;

hence not for C, D being POINT of S holds {A,B,C,D} is planar ; :: thesis: verum