let T be TopStruct ; :: thesis: for M being Subset of T
for F being Subset-Family of T st F is finite holds
F | M is finite
let M be Subset of T; :: thesis: for F being Subset-Family of T st F is finite holds
F | M is finite
let F be Subset-Family of T; :: thesis: ( F is finite implies F | M is finite )
assume A1: F is finite ; :: thesis: F | M is finite
defpred S₁[ set , set ] means for X being Subset of T st X = $1 holds
$2 = X /\ M;
A6: for x being set st x in F holds
ex y being set st S₁[x,y]

proof

let x be set ; :: thesis: ( x in F implies ex y being set st S₁[x,y] )
assume x in F ; :: thesis: ex y being set st S₁[x,y]
then reconsider X = x as Subset of T ;
reconsider y = X /\ M as set ;
take y ; :: thesis: S₁[x,y]
thus S₁[x,y] ; :: thesis: verum

end;

consider f being Function such that
A7: dom f = F and
A8: for x being set st x in F holds
S₁[x,f . x] from CLASSES1:sch 1(A6);
for x being set holds
( x in rng f iff x in F | M )

proof

let x be set ; :: thesis: ( x in rng f iff x in F | M )

hereby :: thesis: ( x in F | M implies x in rng f )

assume x in rng f ; :: thesis: x in F | M
then consider y being set such that
A9: y in dom f and
A10: x = f . y by FUNCT_1:def 5;
reconsider Y = y as Subset of T by A7, A9;
A11: f . y = Y /\ M by A7, A8, A9;
Y /\ M c= M by XBOOLE_1:17;
then Y /\ M c= [#] (T | M) by PRE_TOPC:def 10;
then reconsider X = f . y as Subset of (T | M) by A7, A8, A9;
X in F | M by A7, A9, A11, Def3;
hence x in F | M by A10; :: thesis: verum

end;

assume A12: x in F | M ; :: thesis: x in rng f
then reconsider X = x as Subset of (T | M) ;
consider R being Subset of T such that
A13: R in F and
A14: R /\ M = X by A12, Def3;
f . R = R /\ M by A8, A13;
hence x in rng f by A7, A13, A14, FUNCT_1:def 5; :: thesis: verum

end;

then rng f = F | M by TARSKI:2;
then f .: F = F | M by A7, RELAT_1:146;
hence F | M is finite by A1, FINSET_1:17; :: thesis: verum