let T be TopStruct ; :: thesis: 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 ) ) )
let P be Subset of T; :: thesis: ( ( P = {} implies ( P is compact iff T | P is compact ) ) & ( T is TopSpace-like & P <> {} implies ( P is compact iff T | P is compact ) ) )
A1: [#] (T | P) = P by PRE_TOPC:def 5;
thus ( P = {} implies ( P is compact iff T | P is compact ) ) ; :: thesis: ( T is TopSpace-like & P <> {} implies ( P is compact iff T | P is compact ) )
assume that
A2: T is TopSpace-like and
A3: P <> {} ; :: thesis: ( P is compact iff T | P is compact )
reconsider T9 = T as non empty TopSpace by A2, A3;
reconsider P9 = P as non empty Subset of T9 by A3;
A4: ( [#] (T9 | P9) is compact iff T9 | P9 is compact ) ;
hence ( P is compact implies T | P is compact ) by A1, Th2; :: thesis: ( T | P is compact implies P is compact )
assume T | P is compact ; :: thesis: P is compact
then for Q being Subset of (T | P) st Q = P holds
Q is compact by A4, PRE_TOPC:def 5;
hence P is compact by A1, Th2; :: thesis: verum