theorem Th18: :: COMBGRAS:18

for S1, S2 being IncProjStr
for F being IncProjMap over S1,S2
for K being Subset of the Points of S1 holds F .: K = { B where B is POINT of S2 : ex A being POINT of S1 st
( A in K & F . A = B ) }