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: 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
A3: x in F and
A4: B c= F ; :: thesis: ( not S₁[B] or S₁[B \/ {x}] )
B c= bool the carrier of T

proof

let b be object ; :: 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 A4;
hence b in bool the carrier of T ; :: thesis: verum

end;

then reconsider C = B as Subset-Family of T ;
reconsider X = x as Subset of T by A3;
given A being Subset of T such that A5: A = union B and
A6: A is compact ; :: thesis: S₁[B \/ {x}]
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:25;
hence (union C) \/ X = union (B \/ {x}) by ZFMISC_1:78; :: thesis: (union C) \/ X is compact
X is compact by A1, A3;
hence (union C) \/ X is compact by A5, A6, COMPTS_1:10; :: thesis: verum

end;

A7: S₁[ {} ]

proof

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

end;

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