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 )
assume A1: A <> B ; :: thesis: not for C, D being POINT of S holds {A,B,C,D} is planar
consider P being PLANE of S;
consider C being POINT of S such that
C on P and
A2: not {A,B,C} is linear by A1, Th74;
not for D being POINT of S holds {A,B,C,D} is planar by A2, Th75;
hence not for C, D being POINT of S holds {A,B,C,D} is planar ; :: thesis: verum