let US be non empty upper axiom_U1 UniformSpaceStr ; :: thesis: for x being Element of the carrier of US holds Neighborhood x is upper
let x be Element of US; :: thesis: Neighborhood x is upper
set N = Neighborhood x;
now :: thesis: for S1, S2 being Subset of US st S1 in Neighborhood x & S1 c= S2 holds
S2 in Neighborhood x
let S1, S2 be Subset of US; :: thesis: ( S1 in Neighborhood x & S1 c= S2 implies S2 in Neighborhood x )
assume that
A1: S1 in Neighborhood x and
A2: S1 c= S2 ; :: thesis: S2 in Neighborhood x
consider V1 being Element of the entourages of US such that
A3: S1 = Neighborhood (V1,x) by A1;
A4: V1 c= [:{x},S1:] \/ ([: the carrier of US, the carrier of US:] \ [:{x}, the carrier of US:])
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in V1 or t in [:{x},S1:] \/ ([: the carrier of US, the carrier of US:] \ [:{x}, the carrier of US:]) )
assume A5: t in V1 ; :: thesis: t in [:{x},S1:] \/ ([: the carrier of US, the carrier of US:] \ [:{x}, the carrier of US:])
consider a, b being object such that
a in the carrier of US and
A7: b in the carrier of US and
A8: t = [a,b] by A5, ZFMISC_1:def 2;
reconsider b = b as Element of US by A7;
per cases ( x = a or not x = a ) ;
suppose A9: x = a ; :: thesis: t in [:{x},S1:] \/ ([: the carrier of US, the carrier of US:] \ [:{x}, the carrier of US:])
then ( x in {x} & b in S1 ) by A3, A5, A8, TARSKI:def 1;
then A10: t in [:{x},S1:] by A9, A8, ZFMISC_1:def 2;
[:{x},S1:] c= [:{x},S1:] \/ ([: the carrier of US, the carrier of US:] \ [:{x}, the carrier of US:]) by XBOOLE_1:7;
hence t in [:{x},S1:] \/ ([: the carrier of US, the carrier of US:] \ [:{x}, the carrier of US:]) by A10; :: thesis: verum
end;
suppose A11: not x = a ; :: thesis: t in [:{x},S1:] \/ ([: the carrier of US, the carrier of US:] \ [:{x}, the carrier of US:])
A12: not [a,b] in [:{x}, the carrier of US:]
proof
assume [a,b] in [:{x}, the carrier of US:] ; :: thesis: contradiction
then ex c, d being object st
( c in {x} & d in the carrier of US & [a,b] = [c,d] ) by ZFMISC_1:def 2;
then ( a in {x} & b in the carrier of US ) by XTUPLE_0:1;
hence contradiction by A11, TARSKI:def 1; :: thesis: verum
end;
A13: t in [: the carrier of US, the carrier of US:] \ [:{x}, the carrier of US:] by A5, A12, A8, XBOOLE_0:def 5;
[: the carrier of US, the carrier of US:] \ [:{x}, the carrier of US:] c= [:{x},S1:] \/ ([: the carrier of US, the carrier of US:] \ [:{x}, the carrier of US:]) by XBOOLE_1:7;
hence t in [:{x},S1:] \/ ([: the carrier of US, the carrier of US:] \ [:{x}, the carrier of US:]) by A13; :: thesis: verum
end;
end;
end;
reconsider V2 = [:{x},S2:] \/ ([: the carrier of US, the carrier of US:] \ [:{x}, the carrier of US:]) as Subset of [: the carrier of US, the carrier of US:] ;
A15: V1 c= V2
proof
[:{x},S1:] c= [:{x},S2:] by A2, ZFMISC_1:95;
then [:{x},S1:] \/ ([: the carrier of US, the carrier of US:] \ [:{x}, the carrier of US:]) c= [:{x},S2:] \/ ([: the carrier of US, the carrier of US:] \ [:{x}, the carrier of US:]) by XBOOLE_1:9;
hence V1 c= V2 by A4; :: thesis: verum
end;
US is upper ;
then the entourages of US is upper ;
then reconsider V2 = V2 as Element of the entourages of US by A15;
S2 = Neighborhood (V2,x)
proof
A16: S2 c= Neighborhood (V2,x)
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in S2 or t in Neighborhood (V2,x) )
assume A17: t in S2 ; :: thesis: t in Neighborhood (V2,x)
then reconsider t1 = t as Element of US ;
A18: x in {x} by TARSKI:def 1;
[x,t1] in [:{x},S2:] by A17, A18, ZFMISC_1:def 2;
then [x,t1] in V2 by XBOOLE_0:def 3;
hence t in Neighborhood (V2,x) ; :: thesis: verum
end;
Neighborhood (V2,x) c= S2
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in Neighborhood (V2,x) or t in S2 )
assume t in Neighborhood (V2,x) ; :: thesis: t in S2
then ex y0 being Element of US st
( t = y0 & [x,y0] in V2 ) ;
per cases then ( [x,t] in [:{x},S2:] or [x,t] in [: the carrier of US, the carrier of US:] \ [:{x}, the carrier of US:] ) by XBOOLE_0:def 3;
suppose [x,t] in [:{x},S2:] ; :: thesis: t in S2
then ex a, b being object st
( a in {x} & b in S2 & [x,t] = [a,b] ) by ZFMISC_1:def 2;
hence t in S2 by XTUPLE_0:1; :: thesis: verum
end;
suppose A19: [x,t] in [: the carrier of US, the carrier of US:] \ [:{x}, the carrier of US:] ; :: thesis: t in S2
then ex a, b being object st
( a in the carrier of US & b in the carrier of US & [x,t] = [a,b] ) by ZFMISC_1:def 2;
then A20: t in the carrier of US by XTUPLE_0:1;
x in {x} by TARSKI:def 1;
then [x,t] in [:{x}, the carrier of US:] by A20, ZFMISC_1:def 2;
hence t in S2 by A19, XBOOLE_0:def 5; :: thesis: verum
end;
end;
end;
hence S2 = Neighborhood (V2,x) by A16; :: thesis: verum
end;
hence S2 in Neighborhood x ; :: thesis: verum
end;
hence Neighborhood x is upper ; :: thesis: verum