theorem :: INCSP_1:51

for S being IncSpace
for A being POINT of S ex L, L1, L2 being LINE of S st
( A on L & A on L1 & A on L2 & ( for P being PLANE of S holds
( not L on P or not L1 on P or not L2 on P ) ) )