let X, Y be non empty TopSpace; :: thesis: for F being Subset-Family of X
for H being Subset-Family of [:X,Y:] st F is finite & F c= (Pr1 X,Y) .: H holds
ex G being Subset-Family of [:X,Y:] st
( G c= H & G is finite & F = (Pr1 X,Y) .: G )
let F be Subset-Family of X; :: thesis: for H being Subset-Family of [:X,Y:] st F is finite & F c= (Pr1 X,Y) .: H holds
ex G being Subset-Family of [:X,Y:] st
( G c= H & G is finite & F = (Pr1 X,Y) .: G )
let H be Subset-Family of [:X,Y:]; :: thesis: ( F is finite & F c= (Pr1 X,Y) .: H implies ex G being Subset-Family of [:X,Y:] st
( G c= H & G is finite & F = (Pr1 X,Y) .: G ) )
assume that
A1: F is finite and
A2: F c= (Pr1 X,Y) .: H ; :: thesis: ex G being Subset-Family of [:X,Y:] st
( G c= H & G is finite & F = (Pr1 X,Y) .: G )
defpred S₁[ set , set ] means ( $2 in dom (Pr1 X,Y) & $2 in H & $1 = (Pr1 X,Y) . $2 );
A3: for e being set st e in F holds
ex u being set st S₁[e,u] by A2, FUNCT_1:def 12;
consider f being Function such that
A4: dom f = F and
A5: for e being set st e in F holds
S₁[e,f . e] from CLASSES1:sch 1(A3);
A6: f .: F c= H

proof

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in f .: F or e in H )
assume e in f .: F ; :: thesis: e in H
then ex u being set st
( u in dom f & u in F & e = f . u ) by FUNCT_1:def 12;
hence e in H by A5; :: thesis: verum

end;

then reconsider G = f .: F as Subset-Family of [:X,Y:] by XBOOLE_1:1;
take G ; :: thesis: ( G c= H & G is finite & F = (Pr1 X,Y) .: G )
thus G c= H by A6; :: thesis: ( G is finite & F = (Pr1 X,Y) .: G )
thus G is finite by A1; :: thesis: F = (Pr1 X,Y) .: G

now

let e be set ; :: thesis: ( e in F iff ex u being set st
( u in dom (Pr1 X,Y) & u in G & e = (Pr1 X,Y) . u ) )
thus ( e in F iff ex u being set st
( u in dom (Pr1 X,Y) & u in G & e = (Pr1 X,Y) . u ) ) :: thesis: verum

proof

thus ( e in F implies ex u being set st
( u in dom (Pr1 X,Y) & u in G & e = (Pr1 X,Y) . u ) ) :: thesis: ( ex u being set st
( u in dom (Pr1 X,Y) & u in G & e = (Pr1 X,Y) . u ) implies e in F )

proof

assume A7: e in F ; :: thesis: ex u being set st
( u in dom (Pr1 X,Y) & u in G & e = (Pr1 X,Y) . u )
take f . e ; :: thesis: ( f . e in dom (Pr1 X,Y) & f . e in G & e = (Pr1 X,Y) . (f . e) )
thus f . e in dom (Pr1 X,Y) by A5, A7; :: thesis: ( f . e in G & e = (Pr1 X,Y) . (f . e) )
thus f . e in G by A4, A7, FUNCT_1:def 12; :: thesis: e = (Pr1 X,Y) . (f . e)
thus e = (Pr1 X,Y) . (f . e) by A5, A7; :: thesis: verum

end;

given u being set such that A8: ( u in dom (Pr1 X,Y) & u in G & e = (Pr1 X,Y) . u ) ; :: thesis: e in F
ex v being set st
( v in dom f & v in F & u = f . v ) by A8, FUNCT_1:def 12;
hence e in F by A5, A8; :: thesis: verum

end;

end;

hence F = (Pr1 X,Y) .: G by FUNCT_1:def 12; :: thesis: verum