let T be TopStruct ; :: thesis: ( T is compact iff [#] T is compact )
thus ( T is compact implies [#] T is compact ) :: thesis: ( [#] T is compact implies T is compact )

proof

assume A1: T is compact ; :: thesis: [#] T is compact
let F be Subset-Family of T; :: according to COMPTS_1:def 7 :: thesis: ( F is Cover of [#] T & F is open implies ex G being Subset-Family of T st
( G c= F & G is Cover of [#] T & G is finite ) )
assume that
A2: F is Cover of [#] T and
A3: F is open ; :: thesis: ex G being Subset-Family of T st
( G c= F & G is Cover of [#] T & G is finite )
consider G being Subset-Family of T such that
A4: G c= F and
A5: G is Cover of T and
A6: G is finite by A1, A2, A3, Def3;
take G ; :: thesis: ( G c= F & G is Cover of [#] T & G is finite )
thus ( G c= F & G is Cover of [#] T & G is finite ) by A4, A5, A6; :: thesis: verum

end;

assume A7: [#] T is compact ; :: thesis: T is compact
let F be Subset-Family of T; :: according to COMPTS_1:def 3 :: thesis: ( F is Cover of T & F is open implies ex G being Subset-Family of T st
( G c= F & G is Cover of T & G is finite ) )
assume that
A8: F is Cover of T and
A9: F is open ; :: thesis: ex G being Subset-Family of T st
( G c= F & G is Cover of T & G is finite )
consider G being Subset-Family of T such that
A10: G c= F and
A11: G is Cover of [#] T and
A12: G is finite by A7, A8, A9, Def7;
take G ; :: thesis: ( G c= F & G is Cover of T & G is finite )
thus ( G c= F & G is Cover of T & G is finite ) by A10, A11, A12; :: thesis: verum