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_{1}[ object , object ] means ( $2 in dom (Pr1 (X,Y)) & $2 in H & $1 = (Pr1 (X,Y)) . $2 );

A3: for e being object st e in F holds

ex u being object st S_{1}[e,u]
by A2, FUNCT_1:def 6;

consider f being Function such that

A4: dom f = F and

A5: for e being object st e in F holds

S_{1}[e,f . e]
from CLASSES1:sch 1(A3);

A6: f .: F c= H

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

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

A3: for e being object st e in F holds

ex u being object st S

consider f being Function such that

A4: dom f = F and

A5: for e being object st e in F holds

S

A6: f .: F c= H

proof

then reconsider G = f .: F as Subset-Family of [:X,Y:] by XBOOLE_1:1;
let e be object ; :: 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 object st

( u in dom f & u in F & e = f . u ) by FUNCT_1:def 6;

hence e in H by A5; :: thesis: verum

end;assume e in f .: F ; :: thesis: e in H

then ex u being object st

( u in dom f & u in F & e = f . u ) by FUNCT_1:def 6;

hence e in H by A5; :: thesis: verum

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 :: thesis: for e being object holds

( e in F iff ex u being object st

( u in dom (Pr1 (X,Y)) & u in G & e = (Pr1 (X,Y)) . u ) )

hence
F = (Pr1 (X,Y)) .: G
by FUNCT_1:def 6; :: thesis: verum( e in F iff ex u being object st

( u in dom (Pr1 (X,Y)) & u in G & e = (Pr1 (X,Y)) . u ) )

let e be object ; :: thesis: ( e in F iff ex u being object st

( u in dom (Pr1 (X,Y)) & u in G & e = (Pr1 (X,Y)) . u ) )

thus ( e in F iff ex u being object st

( u in dom (Pr1 (X,Y)) & u in G & e = (Pr1 (X,Y)) . u ) ) :: thesis: verum

end;( u in dom (Pr1 (X,Y)) & u in G & e = (Pr1 (X,Y)) . u ) )

thus ( e in F iff ex u being object 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 object st

( u in dom (Pr1 (X,Y)) & u in G & e = (Pr1 (X,Y)) . u ) ) :: thesis: ( ex u being object st

( u in dom (Pr1 (X,Y)) & u in G & e = (Pr1 (X,Y)) . u ) implies e in F )

A8: u in G and

A9: e = (Pr1 (X,Y)) . u ; :: thesis: e in F

ex v being object st

( v in dom f & v in F & u = f . v ) by A8, FUNCT_1:def 6;

hence e in F by A5, A9; :: thesis: verum

end;( u in dom (Pr1 (X,Y)) & u in G & e = (Pr1 (X,Y)) . u ) ) :: thesis: ( ex u being object st

( u in dom (Pr1 (X,Y)) & u in G & e = (Pr1 (X,Y)) . u ) implies e in F )

proof

given u being object such that
u in dom (Pr1 (X,Y))
and
assume A7:
e in F
; :: thesis: ex u being object 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 6; :: thesis: e = (Pr1 (X,Y)) . (f . e)

thus e = (Pr1 (X,Y)) . (f . e) by A5, A7; :: thesis: verum

end;( 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 6; :: thesis: e = (Pr1 (X,Y)) . (f . e)

thus e = (Pr1 (X,Y)) . (f . e) by A5, A7; :: thesis: verum

A8: u in G and

A9: e = (Pr1 (X,Y)) . u ; :: thesis: e in F

ex v being object st

( v in dom f & v in F & u = f . v ) by A8, FUNCT_1:def 6;

hence e in F by A5, A9; :: thesis: verum