let G be TopologicaladdGroup; :: thesis: for B being Basis of 0_ G
for M being dense Subset of G holds { (V + x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } is Basis of G
let B be Basis of 0_ G; :: thesis: for M being dense Subset of G holds { (V + x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } is Basis of G
let M be dense Subset of G; :: thesis: { (V + x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } is Basis of G
set Z = { (V + x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } ;
A1: { (V + x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } c= the topology of G

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { (V + x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } or a in the topology of G )
assume a in { (V + x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } ; :: thesis: a in the topology of G
then consider V being Subset of G, x being Point of G such that
A2: a = V + x and
A3: V in B and
x in M ;
reconsider V = V as Subset of G ;
V is open by A3, YELLOW_8:12;
hence a in the topology of G by A2, PRE_TOPC:def 2; :: thesis: verum

end;

A4: for W being Subset of G st W is open holds
for a being Point of G st a in W holds
ex V being Subset of G st
( V in { (V + x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } & a in V & V c= W )

proof

A5: (0_ G) + (- (0_ G)) = (0_ G) + (0_ G) by Th8
.= 0_ G by Def4 ;
let W be Subset of G; :: thesis: ( W is open implies for a being Point of G st a in W holds
ex V being Subset of G st
( V in { (V + x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } & a in V & V c= W ) )
assume A6: W is open ; :: thesis: for a being Point of G st a in W holds
ex V being Subset of G st
( V in { (V + x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } & a in V & V c= W )
let a be Point of G; :: thesis: ( a in W implies ex V being Subset of G st
( V in { (V + x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } & a in V & V c= W ) )
assume A7: a in W ; :: thesis: ex V being Subset of G st
( V in { (V + x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } & a in V & V c= W )
0_ G = a + (- a) by Def5;
then W + (- a) is a_neighborhood of (0_ G) + (- (0_ G)) by A7, A6, A5, CONNSP_2:3, Th28;
then consider V being open a_neighborhood of 0_ G such that
A8: V + (- V) c= W + (- a) by Th54;
consider E being Subset of G such that
A9: E in B and
A10: E c= V by CONNSP_2:4, YELLOW_8:13;
( E is open & E <> {} ) by A9, YELLOW_8:12;
then consider d being object such that
A11: d in (a + (- M)) /\ E by XBOOLE_0:4, TOPS_1:45;
reconsider d = d as Point of G by A11;
take I = E + ((- d) + a); :: thesis: ( I in { (V + x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } & a in I & I c= W )
d in a + (- M) by A11, XBOOLE_0:def 4;
then consider m being Point of G such that
A12: d = a + m and
A13: m in - M by Th27;
(- d) + a = ((- d) + a) + (0_ G) by Def4
.= ((- d) + a) + (m + (- m)) by Def5
.= (((- d) + a) + m) + (- m) by RLVECT_1:def 3
.= ((- d) + d) + (- m) by A12, RLVECT_1:def 3
.= (0_ G) + (- m) by Def5
.= - m by Def4 ;
then (- d) + a in M by A13, Th7;
hence I in { (V + x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } by A9; :: thesis: ( a in I & I c= W )
A14: (0_ G) + a = a by Def4;
A15: d in E by A11, XBOOLE_0:def 4;
E + (- d) c= V + (- V)

proof

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in E + (- d) or q in V + (- V) )
assume q in E + (- d) ; :: thesis: q in V + (- V)
then A16: ex v being Point of G st
( q = v + (- d) & v in E ) by Th28;
- d in - V by A10, A15;
hence q in V + (- V) by A10, A16; :: thesis: verum

end;

then E + (- d) c= W + (- a) by A8;
then A17: (E + (- d)) + a c= (W + (- a)) + a by Th5;
d + (- d) = 0_ G by Def5;
then 0_ G in E + (- d) by A15, Th28;
then a in (E + (- d)) + a by A14, Th28;
hence a in I by ThB34; :: thesis: I c= W
(W + (- a)) + a = W + ((- a) + a) by ThB34
.= W + (0_ G) by Def5
.= W by Th37 ;
hence I c= W by A17, ThB34; :: thesis: verum

end;

{ (V + x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } c= bool the carrier of G

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { (V + x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } or a in bool the carrier of G )
assume a in { (V + x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } ; :: thesis: a in bool the carrier of G
then ex V being Subset of G ex x being Point of G st
( a = V + x & V in B & x in M ) ;
hence a in bool the carrier of G ; :: thesis: verum

end;

hence { (V + x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } is Basis of G by A1, A4, YELLOW_9:32; :: thesis: verum