theorem :: COMBGRAS:19

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