let T be non empty Hausdorff TopSpace; :: thesis: for F being Filter of the carrier of T
for p, q being Point of T st p in lim_filter F & q in lim_filter F holds
p = q
let F be Filter of the carrier of T; :: thesis: for p, q being Point of T st p in lim_filter F & q in lim_filter F holds
p = q
let p, q be Point of T; :: thesis: ( p in lim_filter F & q in lim_filter F implies p = q )
assume that
A1: p in lim_filter F and
A2: q in lim_filter F ; :: thesis: p = q
consider p0 being Point of T such that
A3: p = p0 and
A4: F is_filter-finer_than NeighborhoodSystem p0 by A1;
consider q0 being Point of T such that
A5: q = q0 and
A6: F is_filter-finer_than NeighborhoodSystem q0 by A2;
now :: thesis: not p <> q
assume p <> q ; :: thesis: contradiction
then consider G1, G2 being Subset of T such that
A7: G1 is open and
A8: G2 is open and
A9: p in G1 and
A10: q in G2 and
A11: G1 misses G2 by PRE_TOPC:def 10;
( G1 in NeighborhoodSystem p & G2 in NeighborhoodSystem q ) by A7, A8, A9, A10, CONNSP_2:3, YELLOW19:2;
then {} in F by A3, A4, A5, A6, A11, CARD_FIL:def 1;
hence contradiction by CARD_FIL:def 1; :: thesis: verum
end;
hence p = q ; :: thesis: verum