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

proof

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;

hence B is a_neighborhood of A by Def6; :: thesis: verum