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