let X, Y be TopSpace; :: thesis:
let H be Subset-Family of X; :: thesis:
let Y be Subset of X; :: thesis:
assume A1: H is Cover of Y ; :: thesis:
defpred S₁[ set ] means ( $1 in H & $1 /\ Y <> {} );
{ Z where Z is Subset of X : S₁[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:
thus F c= H :: thesis:

let e be object ; :: according to TARSKI:def 3 :: thesis:
assume e in F ; :: thesis:
then ex Z being Subset of X st
( e = Z & Z in H & Z /\ Y <> {} ) ;
hence e in H ; :: thesis:

end;

let e be object ; :: according to TARSKI:def 3,SETFAM_1:def 11 :: thesis:
assume A3: e in Y ; :: thesis:
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:

end;

let C be set ; :: thesis:
assume C in F ; :: thesis:
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: