let ET be non empty strict U_FMT_filter FMT_Space_Str ; :: thesis: for A being non empty Subset of ET holds Neighborhood A is Filter of the carrier of ET
let A be non empty Subset of ET; :: thesis: Neighborhood A is Filter of the carrier of ET
set S = { F where F is a_neighborhood of A : verum } ;
{ F where F is a_neighborhood of A : verum } is Filter of the carrier of ET

proof

A1: { F where F is a_neighborhood of A : verum } is non empty Subset-Family of the carrier of ET

proof

A2: not { F where F is a_neighborhood of A : verum } is empty

proof

set Sq = the carrier of ET;
the carrier of ET c= the carrier of ET ;
then reconsider Sq = the carrier of ET as Subset of the carrier of ET ;
Sq is a_neighborhood of A

proof

for x being Element of ET st x in A holds
Sq in U_FMT x by Th6;
hence Sq is a_neighborhood of A by Def6; :: thesis: verum

end;

then Sq in { F where F is a_neighborhood of A : verum } ;
hence not { F where F is a_neighborhood of A : verum } is empty ; :: thesis: verum

end;

{ F where F is a_neighborhood of A : verum } is Subset-Family of the carrier of ET

proof

{ F where F is a_neighborhood of A : verum } c= bool the carrier of ET

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in { F where F is a_neighborhood of A : verum } or t in bool the carrier of ET )
assume t in { F where F is a_neighborhood of A : verum } ; :: thesis: t in bool the carrier of ET
then consider F0 being a_neighborhood of A such that
A3: t = F0 ;
thus t in bool the carrier of ET by A3; :: thesis: verum

end;

hence { F where F is a_neighborhood of A : verum } is Subset-Family of the carrier of ET ; :: thesis: verum

end;

hence { F where F is a_neighborhood of A : verum } is non empty Subset-Family of the carrier of ET by A2; :: thesis: verum

end;

A4: not {} in { F where F is a_neighborhood of A : verum }

proof

assume {} in { F where F is a_neighborhood of A : verum } ; :: thesis: contradiction
then consider F0 being a_neighborhood of A such that
A5: {} = F0 ;
not A is empty ;
then consider a being object such that
A6: a in A ;
reconsider a0 = a as Element of ET by A6;
A7: {} in U_FMT a0 by A5, A6, Def6;
U_FMT a0 is Filter of the carrier of ET by Def2;
hence contradiction by A7, CARD_FIL:def 1; :: thesis: verum

end;

for Y1, Y2 being Subset of ET holds
( ( Y1 in { F where F is a_neighborhood of A : verum } & Y2 in { F where F is a_neighborhood of A : verum } implies Y1 /\ Y2 in { F where F is a_neighborhood of A : verum } ) & ( Y1 in { F where F is a_neighborhood of A : verum } & Y1 c= Y2 implies Y2 in { F where F is a_neighborhood of A : verum } ) )

proof

let Y1, Y2 be Subset of ET; :: thesis: ( ( Y1 in { F where F is a_neighborhood of A : verum } & Y2 in { F where F is a_neighborhood of A : verum } implies Y1 /\ Y2 in { F where F is a_neighborhood of A : verum } ) & ( Y1 in { F where F is a_neighborhood of A : verum } & Y1 c= Y2 implies Y2 in { F where F is a_neighborhood of A : verum } ) )

now :: thesis: ( Y1 in { F where F is a_neighborhood of A : verum } & Y2 in { F where F is a_neighborhood of A : verum } implies Y1 /\ Y2 in { F where F is a_neighborhood of A : verum } )

assume that
A8: Y1 in { F where F is a_neighborhood of A : verum } and
A9: Y2 in { F where F is a_neighborhood of A : verum } ; :: thesis: Y1 /\ Y2 in { F where F is a_neighborhood of A : verum }
consider F1 being a_neighborhood of A such that
A10: Y1 = F1 by A8;
consider F2 being a_neighborhood of A such that
A11: Y2 = F2 by A9;
A12: for x being Element of ET st x in A holds
Y1 /\ Y2 in U_FMT x

proof

let x be Element of ET; :: thesis: ( x in A implies Y1 /\ Y2 in U_FMT x )
assume x in A ; :: thesis: Y1 /\ Y2 in U_FMT x
then A13: ( Y1 in U_FMT x & Y2 in U_FMT x ) by A10, A11, Def6;
U_FMT x is Filter of the carrier of ET by Def2;
hence Y1 /\ Y2 in U_FMT x by A13, CARD_FIL:def 1; :: thesis: verum

end;

Y1 /\ Y2 is a_neighborhood of A by A12, Def6;
hence Y1 /\ Y2 in { F where F is a_neighborhood of A : verum } ; :: thesis: verum

end;

hence ( Y1 in { F where F is a_neighborhood of A : verum } & Y2 in { F where F is a_neighborhood of A : verum } implies Y1 /\ Y2 in { F where F is a_neighborhood of A : verum } ) ; :: thesis: ( Y1 in { F where F is a_neighborhood of A : verum } & Y1 c= Y2 implies Y2 in { F where F is a_neighborhood of A : verum } )

now :: thesis: ( Y1 in { F where F is a_neighborhood of A : verum } & Y1 c= Y2 & Y1 in { F where F is a_neighborhood of A : verum } & Y1 c= Y2 implies Y2 in { F where F is a_neighborhood of A : verum } )

assume that
A14: Y1 in { F where F is a_neighborhood of A : verum } and
A15: Y1 c= Y2 ; :: thesis: ( Y1 in { F where F is a_neighborhood of A : verum } & Y1 c= Y2 implies Y2 in { F where F is a_neighborhood of A : verum } )
consider y1 being a_neighborhood of A such that
A16: y1 = Y1 by A14;
for x being Element of ET st x in A holds
Y2 in U_FMT x

proof

let x be Element of ET; :: thesis: ( x in A implies Y2 in U_FMT x )
assume x in A ; :: thesis: Y2 in U_FMT x
then A17: Y1 in U_FMT x by A16, Def6;
U_FMT x is Filter of the carrier of ET by Def2;
hence Y2 in U_FMT x by A17, A15, CARD_FIL:def 1; :: thesis: verum

end;

then Y2 is a_neighborhood of A by Def6;
hence ( Y1 in { F where F is a_neighborhood of A : verum } & Y1 c= Y2 implies Y2 in { F where F is a_neighborhood of A : verum } ) ; :: thesis: verum

end;

hence ( Y1 in { F where F is a_neighborhood of A : verum } & Y1 c= Y2 implies Y2 in { F where F is a_neighborhood of A : verum } ) ; :: thesis: verum

end;

hence { F where F is a_neighborhood of A : verum } is Filter of the carrier of ET by A1, A4, CARD_FIL:def 1; :: thesis: verum

end;

hence Neighborhood A is Filter of the carrier of ET ; :: thesis: verum