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 ;
U_FMT x is Filter of the carrier of ET by Def2;
hence Y1 /\ Y2 in U_FMT x by ; :: thesis: verum
end;
Y1 /\ Y2 is a_neighborhood of A by ;
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 ;
U_FMT x is Filter of the carrier of ET by Def2;
hence Y2 in U_FMT x by ; :: 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 ; :: thesis: verum
end;
hence Neighborhood A is Filter of the carrier of ET ; :: thesis: verum