let S, T be TopStruct ; :: thesis: for A being Subset of S
for B being Subset of T st A = B & TopStruct(# the carrier of S,the topology of S #) = TopStruct(# the carrier of T,the topology of T #) & A is compact holds
B is compact
let A be Subset of S; :: thesis: for B being Subset of T st A = B & TopStruct(# the carrier of S,the topology of S #) = TopStruct(# the carrier of T,the topology of T #) & A is compact holds
B is compact
let B be Subset of T; :: thesis: ( A = B & TopStruct(# the carrier of S,the topology of S #) = TopStruct(# the carrier of T,the topology of T #) & A is compact implies B is compact )
assume that
A1: A = B and
A2: TopStruct(# the carrier of S,the topology of S #) = TopStruct(# the carrier of T,the topology of T #) and
A3: for F being Subset-Family of S st F is Cover of A & F is open holds
ex G being Subset-Family of S st
( G c= F & G is Cover of A & G is finite ) ; :: according to COMPTS_1:def 7 :: thesis: B is compact
let F be Subset-Family of T; :: according to COMPTS_1:def 7 :: thesis: ( not F is Cover of B or not F is open or ex b₁ being Element of bool (bool the carrier of T) st
( b₁ c= F & b₁ is Cover of B & b₁ is finite ) )
assume A4: ( F is Cover of B & F is open ) ; :: thesis: ex b₁ being Element of bool (bool the carrier of T) st
( b₁ c= F & b₁ is Cover of B & b₁ is finite )
reconsider K = F as Subset-Family of S by A2;
A5: K is Cover of A by A1, A4;
K is open by A2, A4, WAYBEL_9:19;
then consider L being Subset-Family of S such that
A6: ( L c= K & L is Cover of A & L is finite ) by A3, A5;
reconsider G = L as Subset-Family of T by A2;
take G ; :: thesis: ( G c= F & G is Cover of B & G is finite )
G is Cover of B by A1, A6;
hence ( G c= F & G is Cover of B & G is finite ) by A6; :: thesis: verum