set cB = system_right_uniformity TG;

now :: thesis: ( system_right_uniformity TG is quasi_basis & system_right_uniformity TG is axiom_UP1 & system_right_uniformity TG is axiom_UP2 & system_right_uniformity TG is axiom_UP3 )

now :: thesis: for B1, B2 being Element of system_right_uniformity TG ex B3 being Element of system_right_uniformity TG st B3 c= B1 /\ B2

let B1, B2 be Element of system_right_uniformity TG; :: thesis: ex B3 being Element of system_right_uniformity TG st B3 c= B1 /\ B2
B1 in system_right_uniformity TG ;
then consider U1 being a_neighborhood of 0_ TG such that
A1: B1 = element_right_uniformity U1 ;
B2 in system_right_uniformity TG ;
then consider U2 being a_neighborhood of 0_ TG such that
A2: B2 = element_right_uniformity U2 ;
reconsider U3 = U1 /\ U2 as a_neighborhood of 0_ TG by CONNSP_2:2;
set B3 = element_right_uniformity U3;
element_right_uniformity U3 in system_right_uniformity TG ;
then reconsider B3 = element_right_uniformity U3 as Element of system_right_uniformity TG ;
B3 c= B1 /\ B2

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in B3 or t in B1 /\ B2 )
assume t in B3 ; :: thesis: t in B1 /\ B2
then consider x, y being Element of TG such that
A3: t = [x,y] and
A4: y + (- x) in U3 ;
( y + (- x) in U1 & y + (- x) in U2 ) by A4, XBOOLE_0:def 4;
then ( t in B1 & t in B2 ) by A3, A1, A2;
hence t in B1 /\ B2 by XBOOLE_0:def 4; :: thesis: verum

end;

hence ex B3 being Element of system_right_uniformity TG st B3 c= B1 /\ B2 ; :: thesis: verum

end;

hence system_right_uniformity TG is quasi_basis ; :: thesis: ( system_right_uniformity TG is axiom_UP1 & system_right_uniformity TG is axiom_UP2 & system_right_uniformity TG is axiom_UP3 )

now :: thesis: for B being Element of system_right_uniformity TG holds id the carrier of TG c= B

let B be Element of system_right_uniformity TG; :: thesis: id the carrier of TG c= B
B in system_right_uniformity TG ;
then consider U being a_neighborhood of 0_ TG such that
A5: B = element_right_uniformity U ;

now :: thesis: for t being object st t in id the carrier of TG holds
t in B

let t be object ; :: thesis: ( t in id the carrier of TG implies t in B )
assume A6: t in id the carrier of TG ; :: thesis: t in B
then consider x, y being object such that
A7: x in the carrier of TG and
A8: y in the carrier of TG and
A9: t = [x,y] by ZFMISC_1:def 2;
reconsider x = x, y = y as Element of TG by A7, A8;
x = y by A6, A9, RELAT_1:def 10;
then y + (- x) = 0_ TG by GROUP_1A:def 4;
then ( x is Element of TG & y is Element of TG & y + (- x) in U ) by CONNSP_2:4;
hence t in B by A5, A9; :: thesis: verum

end;

hence id the carrier of TG c= B ; :: thesis: verum

end;

hence system_right_uniformity TG is axiom_UP1 ; :: thesis: ( system_right_uniformity TG is axiom_UP2 & system_right_uniformity TG is axiom_UP3 )

now :: thesis: for B1 being Element of system_right_uniformity TG ex B2 being Element of system_right_uniformity TG st B2 c= B1 ~

let B1 be Element of system_right_uniformity TG; :: thesis: ex B2 being Element of system_right_uniformity TG st B2 c= B1 ~
B1 in system_right_uniformity TG ;
then consider U being a_neighborhood of 0_ TG such that
A10: B1 = element_right_uniformity U ;
consider R1 being Relation of the carrier of TG such that
A11: B1 = R1 and
A12: R1 ~ = B1 ~ ;
- U is a_neighborhood of - (0_ TG) by GROUP_1A:371;
then reconsider U2 = - U as a_neighborhood of 0_ TG by GROUP_1A:8;
set B2 = element_right_uniformity U2;
element_right_uniformity U2 in system_right_uniformity TG ;
then reconsider B2 = element_right_uniformity U2 as Element of system_right_uniformity TG ;
B2 c= B1 ~

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in B2 or t in B1 ~ )
assume t in B2 ; :: thesis: t in B1 ~
then consider a, b being Element of TG such that
A13: t = [a,b] and
A14: b + (- a) in U2 ;
consider g being Element of TG such that
A15: b + (- a) = - g and
A16: g in U by A14;
- (b + (- a)) in U by A15, A16;
then (- (- a)) + (- b) in U by GROUP_1A:16;
then [b,a] in R1 by A10, A11;
hence t in B1 ~ by A12, A13, RELAT_1:def 7; :: thesis: verum

end;

hence ex B2 being Element of system_right_uniformity TG st B2 c= B1 ~ ; :: thesis: verum

end;

hence system_right_uniformity TG is axiom_UP2 ; :: thesis: system_right_uniformity TG is axiom_UP3

now :: thesis: for B1 being Element of system_right_uniformity TG ex B2 being Element of system_right_uniformity TG st B2 * B2 c= B1

let B1 be Element of system_right_uniformity TG; :: thesis: ex B2 being Element of system_right_uniformity TG st B2 * B2 c= B1
B1 in system_right_uniformity TG ;
then consider U being a_neighborhood of 0_ TG such that
A17: B1 = element_right_uniformity U ;
U is a_neighborhood of (0_ TG) + (0_ TG) by GROUP_1A:def 3;
then consider A, B being open a_neighborhood of 0_ TG such that
A17bis: A + B c= U by GROUP_1A:354;
reconsider AB = A /\ B as a_neighborhood of 0_ TG by CONNSP_2:2;
( AB c= A & AB c= B ) by XBOOLE_1:17;
then A18: AB + AB c= A + B by Th3;
set B2 = element_right_uniformity AB;
element_right_uniformity AB in system_right_uniformity TG ;
then reconsider B2 = element_right_uniformity AB as Element of system_right_uniformity TG ;
B2 * B2 c= B1

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in B2 * B2 or t in B1 )
assume A19: t in B2 * B2 ; :: thesis: t in B1
consider R1, R2 being Relation of the carrier of TG such that
A20: R1 = B2 and
R2 = B2 and
B2 * B2 = R1 * R2 ;
t in { [x,y] where x, y is Element of TG : ex z being Element of TG st
( [x,z] in R1 & [z,y] in R1 ) } by A19, A20, UNIFORM2:3;
then consider x, y being Element of TG such that
A23: t = [x,y] and
A24: ex z being Element of TG st
( [x,z] in R1 & [z,y] in R1 ) ;
consider z being Element of TG such that
A25: [x,z] in R1 and
A26: [z,y] in R1 by A24;
consider a, b being Element of TG such that
A27: [x,z] = [a,b] and
A28: b + (- a) in AB by A20, A25;
A29: ( x = a & z = b ) by A27, XTUPLE_0:1;
consider c, d being Element of TG such that
A30: [z,y] = [c,d] and
A31: d + (- c) in AB by A26, A20;
A32: ( z = c & y = d ) by A30, XTUPLE_0:1;
A33: (d + (- c)) + (b + (- a)) = y + ((- z) + (z + (- x))) by A29, A32, RLVECT_1:def 3
.= y + (((- z) + z) + (- x)) by RLVECT_1:def 3
.= y + ((0_ TG) + (- x)) by GROUP_1A:def 4
.= y + (- x) by GROUP_1A:def 3 ;
(d + (- c)) + (b + (- a)) in AB + AB by A28, A31;
then y + (- x) in U by A18, A33, A17bis;
hence t in B1 by A17, A23; :: thesis: verum

end;

hence ex B2 being Element of system_right_uniformity TG st B2 * B2 c= B1 ; :: thesis: verum

end;

hence system_right_uniformity TG is axiom_UP3 ; :: thesis: verum

end;

then ex US being strict UniformSpace st
( the carrier of US = the carrier of TG & the entourages of US = <.(system_right_uniformity TG).] ) by Th7;
hence UniformSpaceStr(# the carrier of TG,<.(system_right_uniformity TG).] #) is non empty UniformSpace ; :: thesis: verum