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 )
defpred S₁[ object , object ] means for X being Subset of T st X = $1 holds
$2 = X /\ M;
A1: for x being object st x in F holds
ex y being object st S₁[x,y]

proof

let x be object ; :: thesis: ( x in F implies ex y being object st S₁[x,y] )
assume x in F ; :: thesis: ex y being object 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
A2: dom f = F and
A3: for x being object st x in F holds
S₁[x,f . x] from CLASSES1:sch 1(A1);
for x being object holds
( x in rng f iff x in F | M )

proof

let x be object ; :: 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 object such that
A4: y in dom f and
A5: x = f . y by FUNCT_1:def 3;
reconsider Y = y as Subset of T by A2, A4;
Y /\ M c= M by XBOOLE_1:17;
then Y /\ M c= [#] (T | M) by PRE_TOPC:def 5;
then reconsider X = f . y as Subset of (T | M) by A2, A3, A4;
f . y = Y /\ M by A2, A3, A4;
then X in F | M by A2, A4, Def3;
hence x in F | M by A5; :: thesis: verum

end;

assume A6: 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
A7: R in F and
A8: R /\ M = X by A6, Def3;
f . R = R /\ M by A3, A7;
hence x in rng f by A2, A7, A8, FUNCT_1:def 3; :: thesis: verum

end;

then rng f = F | M by TARSKI:2;
then A9: f .: F = F | M by A2, RELAT_1:113;
assume F is finite ; :: thesis: F | M is finite
hence F | M is finite by A9, FINSET_1:5; :: thesis: verum