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

( ( 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