theorem Th8: :: MESFUN16:8

for P, Q being RealNormSpace
for E being Subset of P
for F being Subset of Q st E is compact & F is compact holds
( [:E,F:] is Subset of [:P,Q:] & [:E,F:] is compact )