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 Th74;
not for D being POINT of S holds {A,B,C,D} is planar by A1, Th75;
hence not for C, D being POINT of S holds {A,B,C,D} is planar ; :: thesis: verum