let NT be T_2 NTopSpace; :: thesis: for x, y being Point of NT st x <> y holds
ex Vx being Element of U_FMT x ex Vy being Element of U_FMT y st Vx misses Vy
let x, y be Point of NT; :: thesis: ( x <> y implies ex Vx being Element of U_FMT x ex Vy being Element of U_FMT y st Vx misses Vy )
assume A1: x <> y ; :: thesis: ex Vx being Element of U_FMT x ex Vy being Element of U_FMT y st Vx misses Vy
now :: thesis: not for Vx being Element of U_FMT x
for Vy being Element of U_FMT y holds Vx meets Vy
assume A2: for Vx being Element of U_FMT x
for Vy being Element of U_FMT y holds Vx meets Vy ; :: thesis: contradiction
A3: now :: thesis: for Vx being Element of U_FMT x
for Vy being Element of U_FMT y holds not Vx /\ Vy is empty
let Vx be Element of U_FMT x; :: thesis: for Vy being Element of U_FMT y holds not Vx /\ Vy is empty
let Vy be Element of U_FMT y; :: thesis: not Vx /\ Vy is empty
Vx meets Vy by A2;
hence not Vx /\ Vy is empty ; :: thesis: verum
end;
reconsider X = the carrier of NT as non empty set ;
reconsider Ux = U_FMT x as Filter of X ;
reconsider Uy = U_FMT y as Filter of X ;
consider F being Filter of X such that
A4: F is_filter-finer_than Ux and
A5: F is_filter-finer_than Uy by A3, CARDFIL2:58;
reconsider x9 = x, y9 = y as Element of X ;
reconsider F = F as Filter of the carrier of NT ;
A6: ( x9 in lim_filter F & y9 in lim_filter F ) by A4, A5;
( lim_filter F is empty or lim_filter F is trivial ) by Def12;
hence contradiction by A1, A6; :: thesis: verum
end;
hence ex Vx being Element of U_FMT x ex Vy being Element of U_FMT y st Vx misses Vy ; :: thesis: verum