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

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

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

( ( 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 } ) )

end;proof

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

end;proof

{ F where F is a_neighborhood of A : verum } is Subset-Family of the carrier of ET
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

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

end;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

then
Sq in { F where F is a_neighborhood of A : verum }
;
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;Sq in U_FMT x by Th6;

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

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

proof

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

end;proof

hence
{ F where F is a_neighborhood of A : verum } is Subset-Family of the carrier of ET
; :: thesis: verum
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;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

proof

for Y1, Y2 being Subset of ET holds
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;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

( ( 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

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
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 } ) )

end;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 } )

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 } )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

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

end;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

Y1 /\ Y2 is a_neighborhood of A
by A12, Def6;
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;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

hence Y1 /\ Y2 in { F where F is a_neighborhood of A : verum } ; :: thesis: 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 } )

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: verumassume 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

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;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

then
Y2 is a_neighborhood of A
by Def6;
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;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

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