theorem Th23: :: INCSP_1:23

for S being IncSpace
for K, L being LINE of S st ex A being POINT of S st
( A on K & A on L ) holds
ex P being PLANE of S st
( K on P & L on P )