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

now :: thesis: for Y1, Y2 being set st Y1 in Neighborhood x & Y2 in Neighborhood x holds
Y1 /\ Y2 in Neighborhood x

let Y1, Y2 be set ; :: thesis: ( Y1 in Neighborhood x & Y2 in Neighborhood x implies Y1 /\ Y2 in Neighborhood x )
assume that
A1: Y1 in Neighborhood x and
A2: Y2 in Neighborhood x ; :: thesis: Y1 /\ Y2 in Neighborhood x
consider V1 being Element of the entourages of US such that
A3: Y1 = Neighborhood (V1,x) by A1;
consider V2 being Element of the entourages of US such that
A4: Y2 = Neighborhood (V2,x) by A2;
Y1 /\ Y2 = Neighborhood ((V1 /\ V2),x) by A3, A4, Th11;
hence Y1 /\ Y2 in Neighborhood x ; :: thesis: verum

end;

hence Neighborhood x is cap-closed by FINSUB_1:def 2; :: thesis: verum