let X, Y be TopSpace; :: thesis: for H being Subset-Family of X

for Y being Subset of X st H is Cover of Y holds

ex F being Subset-Family of X st

( F c= H & F is Cover of Y & ( for C being set st C in F holds

C meets Y ) )

let H be Subset-Family of X; :: thesis: for Y being Subset of X st H is Cover of Y holds

ex F being Subset-Family of X st

( F c= H & F is Cover of Y & ( for C being set st C in F holds

C meets Y ) )

let Y be Subset of X; :: thesis: ( H is Cover of Y implies ex F being Subset-Family of X st

( F c= H & F is Cover of Y & ( for C being set st C in F holds

C meets Y ) ) )

assume A1: H is Cover of Y ; :: thesis: ex F being Subset-Family of X st

( F c= H & F is Cover of Y & ( for C being set st C in F holds

C meets Y ) )

defpred S_{1}[ set ] means ( $1 in H & $1 /\ Y <> {} );

{ Z where Z is Subset of X : S_{1}[Z] } is Subset-Family of X
from DOMAIN_1:sch 7();

then reconsider F = { Z where Z is Subset of X : ( Z in H & Z /\ Y <> {} ) } as Subset-Family of X ;

reconsider F = F as Subset-Family of X ;

take F ; :: thesis: ( F c= H & F is Cover of Y & ( for C being set st C in F holds

C meets Y ) )

thus F c= H :: thesis: ( F is Cover of Y & ( for C being set st C in F holds

C meets Y ) )

thus F is Cover of Y :: thesis: for C being set st C in F holds

C meets Y

assume C in F ; :: thesis: C meets Y

then ex Z being Subset of X st

( C = Z & Z in H & Z /\ Y <> {} ) ;

hence C /\ Y <> {} ; :: according to XBOOLE_0:def 7 :: thesis: verum

for Y being Subset of X st H is Cover of Y holds

ex F being Subset-Family of X st

( F c= H & F is Cover of Y & ( for C being set st C in F holds

C meets Y ) )

let H be Subset-Family of X; :: thesis: for Y being Subset of X st H is Cover of Y holds

ex F being Subset-Family of X st

( F c= H & F is Cover of Y & ( for C being set st C in F holds

C meets Y ) )

let Y be Subset of X; :: thesis: ( H is Cover of Y implies ex F being Subset-Family of X st

( F c= H & F is Cover of Y & ( for C being set st C in F holds

C meets Y ) ) )

assume A1: H is Cover of Y ; :: thesis: ex F being Subset-Family of X st

( F c= H & F is Cover of Y & ( for C being set st C in F holds

C meets Y ) )

defpred S

{ Z where Z is Subset of X : S

then reconsider F = { Z where Z is Subset of X : ( Z in H & Z /\ Y <> {} ) } as Subset-Family of X ;

reconsider F = F as Subset-Family of X ;

take F ; :: thesis: ( F c= H & F is Cover of Y & ( for C being set st C in F holds

C meets Y ) )

thus F c= H :: thesis: ( F is Cover of Y & ( for C being set st C in F holds

C meets Y ) )

proof

A2:
Y c= union H
by A1, SETFAM_1:def 11;
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in F or e in H )

assume e in F ; :: thesis: e in H

then ex Z being Subset of X st

( e = Z & Z in H & Z /\ Y <> {} ) ;

hence e in H ; :: thesis: verum

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

then ex Z being Subset of X st

( e = Z & Z in H & Z /\ Y <> {} ) ;

hence e in H ; :: thesis: verum

thus F is Cover of Y :: thesis: for C being set st C in F holds

C meets Y

proof

let C be set ; :: thesis: ( C in F implies C meets Y )
let e be object ; :: according to TARSKI:def 3,SETFAM_1:def 11 :: thesis: ( not e in Y or e in union F )

assume A3: e in Y ; :: thesis: e in union F

then consider u being set such that

A4: e in u and

A5: u in H by A2, TARSKI:def 4;

reconsider u = u as Subset of X by A5;

u /\ Y <> {} by A3, A4, XBOOLE_0:def 4;

then u in F by A5;

hence e in union F by A4, TARSKI:def 4; :: thesis: verum

end;assume A3: e in Y ; :: thesis: e in union F

then consider u being set such that

A4: e in u and

A5: u in H by A2, TARSKI:def 4;

reconsider u = u as Subset of X by A5;

u /\ Y <> {} by A3, A4, XBOOLE_0:def 4;

then u in F by A5;

hence e in union F by A4, TARSKI:def 4; :: thesis: verum

assume C in F ; :: thesis: C meets Y

then ex Z being Subset of X st

( C = Z & Z in H & Z /\ Y <> {} ) ;

hence C /\ Y <> {} ; :: according to XBOOLE_0:def 7 :: thesis: verum