let T be non empty TopSpace; :: thesis: for FX being Subset-Family of T
for W being Subset of T holds { V where V is Subset of T : ( V in FX & V meets W ) } c= FX
let FX be Subset-Family of T; :: thesis: for W being Subset of T holds { V where V is Subset of T : ( V in FX & V meets W ) } c= FX
let W be Subset of T; :: thesis: { V where V is Subset of T : ( V in FX & V meets W ) } c= FX

now :: thesis: for Y being object st Y in { V where V is Subset of T : ( V in FX & V meets W ) } holds
Y in FX

let Y be object ; :: thesis: ( Y in { V where V is Subset of T : ( V in FX & V meets W ) } implies Y in FX )
assume Y in { V where V is Subset of T : ( V in FX & V meets W ) } ; :: thesis: Y in FX
then ex V being Subset of T st
( Y = V & V in FX & V meets W ) ;
hence Y in FX ; :: thesis: verum

end;

hence { V where V is Subset of T : ( V in FX & V meets W ) } c= FX ; :: thesis: verum