let ET be FMT_TopSpace; :: thesis: for cF being Filter of the carrier of ET
for cS being non empty Subset of cF
for A being non empty Subset of ET st cF = Neighborhood A & cS = OpenNeighborhoods A holds
cS is filter_basis
let cF be Filter of the carrier of ET; :: thesis: for cS being non empty Subset of cF
for A being non empty Subset of ET st cF = Neighborhood A & cS = OpenNeighborhoods A holds
cS is filter_basis
let cS be non empty Subset of cF; :: thesis: for A being non empty Subset of ET st cF = Neighborhood A & cS = OpenNeighborhoods A holds
cS is filter_basis
let A be non empty Subset of ET; :: thesis: ( cF = Neighborhood A & cS = OpenNeighborhoods A implies cS is filter_basis )
assume that
A1: cF = Neighborhood A and
A2: cS = OpenNeighborhoods A ; :: thesis: cS is filter_basis
for f being Element of cF ex b being Element of cS st b c= f

proof

let f be Element of cF; :: thesis: ex b being Element of cS st b c= f
f in { N where N is a_neighborhood of A : verum } by A1;
then consider N being a_neighborhood of A such that
A3: f = N ;
consider O being open Subset of ET such that
A4: ( A c= O & O c= N ) by Th11;
O is open ;
then for x being Element of ET st x in A holds
O in U_FMT x by A4;
then O is open a_neighborhood of A by Def6;
then O in { N where N is open a_neighborhood of A : verum } ;
hence ex b being Element of cS st b c= f by A2, A3, A4; :: thesis: verum

end;

hence cS is filter_basis ; :: thesis: verum