let X be TopStruct ; :: thesis: for Y being SubSpace of X
for A being Subset of
for B being Subset of st A = B holds
( A is compact iff B is compact )
let Y be SubSpace of X; :: thesis: for A being Subset of
for B being Subset of st A = B holds
( A is compact iff B is compact )
let A be Subset of ; :: thesis: for B being Subset of st A = B holds
( A is compact iff B is compact )
let B be Subset of ; :: 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, Th11; :: thesis: ( B is compact implies A is compact )
assume B is compact ; :: thesis: A is compact
then for P being Subset of st P = A holds
P is compact by A1;
hence A is compact by A1, A2, Th11; :: thesis: verum