let T be TopSpace; :: thesis:
let F be finite Subset-Family of T; :: thesis:
assume A1: for X being Subset of T st X in F holds
X is compact ; :: thesis:
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}]

let x, B be set ; :: thesis:
assume that
A3: x in F and
A4: B c= F ; :: thesis:
B c= bool the carrier of T

let b be object ; :: according to TARSKI:def 3 :: thesis:
assume b in B ; :: thesis:
then b in F by A4;
hence b in bool the carrier of T ; :: thesis:

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:
set K = (union C) \/ X;
take (union C) \/ X ; :: thesis:
union {x} = x by ZFMISC_1:25;
hence (union C) \/ X = union (B \/ {x}) by ZFMISC_1:78; :: thesis:
X is compact by A1, A3;
hence (union C) \/ X is compact by A5, A6, COMPTS_1:10; :: thesis:

end;

end;