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