let X be TopStruct ; :: thesis: for Y being SubSpace of X

for A being Subset of X

for B being Subset of Y st A = B holds

( A is compact iff B is compact )

let Y be SubSpace of X; :: thesis: for A being Subset of X

for B being Subset of Y st A = B holds

( A is compact iff B is compact )

let A be Subset of X; :: thesis: for B being Subset of Y st A = B holds

( A is compact iff B is compact )

let B be Subset of Y; :: thesis: ( A = B implies ( A is compact iff B is compact ) )

assume A1: A = B ; :: thesis: ( A is compact iff B is compact )

A2: B c= [#] Y ;

hence ( A is compact implies B is compact ) by A1, Th2; :: thesis: ( B is compact implies A is compact )

assume B is compact ; :: thesis: A is compact

then for P being Subset of Y st P = A holds

P is compact by A1;

hence A is compact by A1, A2, Th2; :: thesis: verum

for A being Subset of X

for B being Subset of Y st A = B holds

( A is compact iff B is compact )

let Y be SubSpace of X; :: thesis: for A being Subset of X

for B being Subset of Y st A = B holds

( A is compact iff B is compact )

let A be Subset of X; :: thesis: for B being Subset of Y st A = B holds

( A is compact iff B is compact )

let B be Subset of Y; :: thesis: ( A = B implies ( A is compact iff B is compact ) )

assume A1: A = B ; :: thesis: ( A is compact iff B is compact )

A2: B c= [#] Y ;

hence ( A is compact implies B is compact ) by A1, Th2; :: thesis: ( B is compact implies A is compact )

assume B is compact ; :: thesis: A is compact

then for P being Subset of Y st P = A holds

P is compact by A1;

hence A is compact by A1, A2, Th2; :: thesis: verum