let US be non empty upper cap-closed axiom_U1 UniformSpaceStr ; :: thesis:
let x be Element of US; :: thesis:
set N = Neighborhood x;

now :: thesis:

thus not {} in Neighborhood x :: thesis:

proof

assume {} in Neighborhood x ; :: thesis:
then ex V being Element of the entourages of US st {} = Neighborhood (V,x) ;
hence contradiction ; :: thesis:

end;

hereby :: thesis:

let Y1, Y2 be Subset of US; :: thesis:

hereby :: thesis:

assume that
A1: Y1 in Neighborhood x and
A2: Y2 in Neighborhood x ; :: thesis:
Neighborhood x is cap-closed by Th17;
hence Y1 /\ Y2 in Neighborhood x by A1, A2, FINSUB_1:def 2; :: thesis:

end;

hereby :: thesis:

assume that
A3: Y1 in Neighborhood x and
A4: Y1 c= Y2 ; :: thesis:
Neighborhood x is upper by Th15;
hence Y2 in Neighborhood x by A3, A4; :: thesis:

end;

end;

end;

hence Neighborhood x is Filter of the carrier of US by CARD_FIL:def 1; :: thesis: