for T being TopSpace
for A being Subset of T
for F being Subset-Family of T holds card (F | A) c= card F