for T being TopStruct
for P being Subset of T holds
( ( P = {} implies ( P is compact iff T | P is compact ) ) & ( T is TopSpace-like & P <> {} implies ( P is compact iff T | P is compact ) ) )