theorem Th25: :: TOPGEN_4:25

for T being set
for F, G being Subset-Family of T holds card (INTERSECTION (F,G)) c= card [:F,G:]