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 4 :: thesis: B is compact
let F be Subset-Family of T; :: according to COMPTS_1:def 4 :: thesis: ( not F is Cover of B or not F is open or ex b₁ being Element of K6(K6( 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 K6(K6( 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;
consider L being Subset-Family of S such that
A5: ( L c= K & L is Cover of A & L is finite ) by A1, A2, A3, A4, WAYBEL_9:19;
reconsider G = L as Subset-Family of T by A2;
take G ; :: thesis: ( G c= F & G is Cover of B & G is finite )
thus ( G c= F & G is Cover of B & G is finite ) by A1, A5; :: thesis: verum