let T be non empty TopSpace; :: thesis: for X being non empty Subset of T
for FX being Subset-Family of T st FX is Cover of X holds
for x being Point of T st x in X holds
ex W being Subset of T st
( x in W & W in FX )
let X be non empty Subset of T; :: thesis: for FX being Subset-Family of T st FX is Cover of X holds
for x being Point of T st x in X holds
ex W being Subset of T st
( x in W & W in FX )
let FX be Subset-Family of T; :: thesis: ( FX is Cover of X implies for x being Point of T st x in X holds
ex W being Subset of T st
( x in W & W in FX ) )
assume FX is Cover of X ; :: thesis: for x being Point of T st x in X holds
ex W being Subset of T st
( x in W & W in FX )
then A1: X c= union FX by SETFAM_1:def 11;
let x be Point of T; :: thesis: ( x in X implies ex W being Subset of T st
( x in W & W in FX ) )
assume x in X ; :: thesis: ex W being Subset of T st
( x in W & W in FX )
then consider W being set such that
A2: x in W and
A3: W in FX by A1, TARSKI:def 4;
reconsider W = W as Subset of T by A3;
take W ; :: thesis: ( x in W & W in FX )
thus ( x in W & W in FX ) by A2, A3; :: thesis: verum