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

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

hence
cS is filter_basis
; :: thesis: verum
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;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