let T1, T2 be non empty compact TopSpace; :: thesis: [:T1,T2:] is compact
set T = [:T1,T2:];
let F be Subset-Family of [:T1,T2:]; :: according to COMPTS_1:def 1 :: thesis: ( not F is Cover of the carrier of [:T1,T2:] or not F is open or ex b₁ being Element of bool (bool the carrier of [:T1,T2:]) st
( b₁ c= F & b₁ is Cover of the carrier of [:T1,T2:] & b₁ is finite ) )
assume ( F is Cover of [:T1,T2:] & F is open ) ; :: thesis: ex b₁ being Element of bool (bool the carrier of [:T1,T2:]) st
( b₁ c= F & b₁ is Cover of the carrier of [:T1,T2:] & b₁ is finite )
hence ex b₁ being Element of bool (bool the carrier of [:T1,T2:]) st
( b₁ c= F & b₁ is Cover of the carrier of [:T1,T2:] & b₁ is finite ) by Th23; :: thesis: verum