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 ; :: according to COMPTS_1:def 3 :: thesis: ( F is Cover of & F is open implies ex G being Subset-Family of st
( G c= F & G is Cover of & G is finite ) )
assume that
A2: F is Cover of and
F is open ; :: thesis: ex G being Subset-Family of st
( G c= F & G is Cover of & G is finite )
take F ; :: thesis: ( F c= F & F is Cover of & F is finite )
thus ( F c= F & F is Cover of ) by A2; :: thesis: F is finite
thus F is finite by A1; :: thesis: verum