theorem :: INCSP_1:42

for S being IncSpace
for P being PLANE of S ex A, B, C, D being POINT of S st
( A on P & not {A,B,C,D} is planar ) by Lm2;