let T be non empty TopSpace; :: thesis:
let FX be Subset-Family of T; :: thesis:
assume FX is Cover of T ; :: thesis:
then A1: union FX = [#] T by SETFAM_1:45;
thus for x being Point of T ex W being Subset of T st
( x in W & W in FX ) :: thesis:

proof

let x be Point of T; :: thesis:
thus ex W being Subset of T st
( x in W & W in FX ) :: thesis:

proof

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:
thus ( x in W & W in FX ) by A2, A3; :: thesis:

end;

end;