let T be TopSpace; :: thesis: for F being finite Subset-Family of T st ( for X being Subset of T st X in F holds
X is compact ) holds
union F is compact
let F be finite Subset-Family of T; :: thesis: ( ( for X being Subset of T st X in F holds
X is compact ) implies union F is compact )
assume A1: for X being Subset of T st X in F holds
X is compact ; :: thesis: union F is compact
defpred S₁[ set ] means ex A being Subset of T st
( A = union $1 & A is compact );
A2: F is finite ;
A3: S₁[ {} ]

proof

take {} T ; :: thesis: ( {} T = union {} & {} T is compact )
thus ( {} T = union {} & {} T is compact ) by ZFMISC_1:2; :: thesis: verum

end;

A4: for x, B being set st x in F & B c= F & S₁[B] holds
S₁[B \/ {x}]

proof

let x, B be set ; :: thesis: ( x in F & B c= F & S₁[B] implies S₁[B \/ {x}] )
assume that
A5: x in F and
A6: B c= F ; :: thesis: ( not S₁[B] or S₁[B \/ {x}] )
given A being Subset of T such that A7: A = union B and
A8: A is compact ; :: thesis: S₁[B \/ {x}]
reconsider X = x as Subset of T by A5;
B c= bool the carrier of T

proof

let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in B or b in bool the carrier of T )
assume b in B ; :: thesis: b in bool the carrier of T
then b in F by A6;
hence b in bool the carrier of T ; :: thesis: verum

end;

then reconsider C = B as Subset-Family of T ;
set K = (union C) \/ X;
take (union C) \/ X ; :: thesis: ( (union C) \/ X = union (B \/ {x}) & (union C) \/ X is compact )
union {x} = x by ZFMISC_1:31;
hence (union C) \/ X = union (B \/ {x}) by ZFMISC_1:96; :: thesis: (union C) \/ X is compact
X is compact by A1, A5;
hence (union C) \/ X is compact by A7, A8, COMPTS_1:19; :: thesis: verum

end;

S₁[F] from FINSET_1:sch 2(A2, A3, A4);
hence union F is compact ; :: thesis: verum