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 10;
thus ( P = {} implies ( P is compact iff T | P is compact ) ) by Th10, A1; :: thesis: ( T is TopSpace-like & P <> {} implies ( P is compact iff T | P is compact ) )
assume that
A3: T is TopSpace-like and
A4: P <> {} ; :: thesis: ( P is compact iff T | P is compact )
reconsider T' = T as non empty TopSpace by A3, A4;
reconsider P' = P as non empty Subset of T' by A4;
A5: ( [#] (T' | P') is compact iff T' | P' is compact ) by Th10;
hence ( P is compact implies T | P is compact ) by A1, Th11; :: 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 A5, PRE_TOPC:def 10;
hence P is compact by A1, Th11; :: thesis: verum