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 1_ TG such that
A1: B1 = element_right_uniformity U1 ;
B2 in system_right_uniformity TG ;
then consider U2 being a_neighborhood of 1_ TG such that
A2: B2 = element_right_uniformity U2 ;
reconsider U3 = U1 /\ U2 as a_neighborhood of 1_ 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 1_ 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 ") = 1_ TG by GROUP_1:def 5;
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 1_ 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 (1_ TG) " by TOPGRP_1:54;
then reconsider U2 = U " as a_neighborhood of 1_ TG by GROUP_1: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_1:17;
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 1_ TG such that
A17: B1 = element_right_uniformity U ;
U is a_neighborhood of (1_ TG) * (1_ TG) by GROUP_1:def 4;
then consider A, B being open a_neighborhood of 1_ TG such that
A17bis: A * B c= U by TOPGRP_1:37;
reconsider AB = A /\ B as a_neighborhood of 1_ TG by CONNSP_2:2;
( AB c= A & AB c= B ) by XBOOLE_1:17;
then A18: AB * AB c= A * B by GROUP_3:4;
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, GROUP_1:def 3
.= y * (((z ") * z) * (x ")) by GROUP_1:def 3
.= y * ((1_ TG) * (x ")) by GROUP_1:def 5
.= y * (x ") by GROUP_1:def 4 ;
(d * (c ")) * (b * (a ")) in AB * AB by A31, A28;
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