let T be TopSpace; :: thesis: ( T is finite implies T is compact )
assume A1: the carrier of T is finite ; :: according to STRUCT_0:def 11 :: thesis: T is compact
let F be Subset-Family of T; :: according to COMPTS_1:def 1 :: 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
F is open ; :: thesis: ex G being Subset-Family of T st
( G c= F & G is Cover of T & G is finite )
take F ; :: thesis: ( F c= F & F is Cover of T & F is finite )
thus ( F c= F & F is Cover of T ) by A2; :: thesis: F is finite
thus F is finite by A1; :: thesis: verum