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