let ET be non empty strict U_FMT_filter FMT_Space_Str ; :: thesis: for A being Subset of ET

for NA being a_neighborhood of A

for B being Subset of ET st NA c= B holds

B is a_neighborhood of A

let A be Subset of ET; :: thesis: for NA being a_neighborhood of A

for B being Subset of ET st NA c= B holds

B is a_neighborhood of A

let NA be a_neighborhood of A; :: thesis: for B being Subset of ET st NA c= B holds

B is a_neighborhood of A

let B be Subset of ET; :: thesis: ( NA c= B implies B is a_neighborhood of A )

assume A1: NA c= B ; :: thesis: B is a_neighborhood of A

for x being Element of ET st x in A holds

B in U_FMT x

for NA being a_neighborhood of A

for B being Subset of ET st NA c= B holds

B is a_neighborhood of A

let A be Subset of ET; :: thesis: for NA being a_neighborhood of A

for B being Subset of ET st NA c= B holds

B is a_neighborhood of A

let NA be a_neighborhood of A; :: thesis: for B being Subset of ET st NA c= B holds

B is a_neighborhood of A

let B be Subset of ET; :: thesis: ( NA c= B implies B is a_neighborhood of A )

assume A1: NA c= B ; :: thesis: B is a_neighborhood of A

for x being Element of ET st x in A holds

B in U_FMT x

proof

hence
B is a_neighborhood of A
by Def6; :: thesis: verum
let x be Element of ET; :: thesis: ( x in A implies B in U_FMT x )

assume x in A ; :: thesis: B in U_FMT x

then A2: NA in U_FMT x by Def6;

U_FMT x is Filter of the carrier of ET by Def2;

hence B in U_FMT x by A1, A2, CARD_FIL:def 1; :: thesis: verum

end;assume x in A ; :: thesis: B in U_FMT x

then A2: NA in U_FMT x by Def6;

U_FMT x is Filter of the carrier of ET by Def2;

hence B in U_FMT x by A1, A2, CARD_FIL:def 1; :: thesis: verum