let US be non empty upper cap-closed axiom_U1 UniformSpaceStr ; :: thesis: for x being Element of US holds Neighborhood x is Filter of the carrier of US
let x be Element of US; :: thesis: Neighborhood x is Filter of the carrier of US
set N = Neighborhood x;

now :: thesis: ( not {} in Neighborhood x & ( for Y1, Y2 being Subset of US holds
( ( Y1 in Neighborhood x & Y2 in Neighborhood x implies Y1 /\ Y2 in Neighborhood x ) & ( Y1 in Neighborhood x & Y1 c= Y2 implies Y2 in Neighborhood x ) ) ) )

thus not {} in Neighborhood x :: thesis: for Y1, Y2 being Subset of US holds
( ( Y1 in Neighborhood x & Y2 in Neighborhood x implies Y1 /\ Y2 in Neighborhood x ) & ( Y1 in Neighborhood x & Y1 c= Y2 implies Y2 in Neighborhood x ) )

proof

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

end;

hereby :: thesis: verum

let Y1, Y2 be Subset of US; :: thesis: ( ( Y1 in Neighborhood x & Y2 in Neighborhood x implies Y1 /\ Y2 in Neighborhood x ) & ( Y1 in Neighborhood x & Y1 c= Y2 implies Y2 in Neighborhood x ) )

hereby :: thesis: ( Y1 in Neighborhood x & Y1 c= Y2 implies Y2 in Neighborhood x )

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

end;

hereby :: thesis: verum

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

end;

end;

end;

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