for T being TopStruct
for P being Subset of T
for F being Subset-Family of T ex f being Function st
( dom f = F & rng f = F | P & ( for x being set st x in F holds
for Q being Subset of T st Q = x holds
f . x = Q /\ P ) )