set cB = system_left_uniformity TG;

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

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

let B1, B2 be Element of system_left_uniformity TG; :: thesis: ex B3 being Element of system_left_uniformity TG st B3 c= B1 /\ B2
B1 in system_left_uniformity TG ;
then consider U1 being a_neighborhood of 1_ TG such that
A1: B1 = element_left_uniformity U1 ;
B2 in system_left_uniformity TG ;
then consider U2 being a_neighborhood of 1_ TG such that
A2: B2 = element_left_uniformity U2 ;
reconsider U3 = U1 /\ U2 as a_neighborhood of 1_ TG by CONNSP_2:2;
set B3 = element_left_uniformity U3;
element_left_uniformity U3 in system_left_uniformity TG ;
then reconsider B3 = element_left_uniformity U3 as Element of system_left_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: (x ") * y in U3 ;
( (x ") * y in U1 & (x ") * y 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_left_uniformity TG st B3 c= B1 /\ B2 ; :: thesis: verum

end;

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

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

let B be Element of system_left_uniformity TG; :: thesis: id the carrier of TG c= B
B in system_left_uniformity TG ;
then consider U being a_neighborhood of 1_ TG such that
A5: B = element_left_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 (x ") * y = 1_ TG by GROUP_1:def 5;
then ( x is Element of TG & y is Element of TG & (x ") * y 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_left_uniformity TG is axiom_UP1 ; :: thesis: ( system_left_uniformity TG is axiom_UP2 & system_left_uniformity TG is axiom_UP3 )

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

let B1 be Element of system_left_uniformity TG; :: thesis: ex B2 being Element of system_left_uniformity TG st B2 c= B1 ~
B1 in system_left_uniformity TG ;
then consider U being a_neighborhood of 1_ TG such that
A10: B1 = element_left_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_left_uniformity U2;
element_left_uniformity U2 in system_left_uniformity TG ;
then reconsider B2 = element_left_uniformity U2 as Element of system_left_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: (a ") * b in U2 ;
consider g being Element of TG such that
A15: (a ") * b = g " and
A16: g in U by A14;
((a ") * b) " in U by A15, A16;
then (b ") * ((a ") ") 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_left_uniformity TG st B2 c= B1 ~ ; :: thesis: verum

end;

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

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

let B1 be Element of system_left_uniformity TG; :: thesis: ex B2 being Element of system_left_uniformity TG st B2 * B2 c= B1
B1 in system_left_uniformity TG ;
then consider U being a_neighborhood of 1_ TG such that
A17: B1 = element_left_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_left_uniformity AB;
element_left_uniformity AB in system_left_uniformity TG ;
then reconsider B2 = element_left_uniformity AB as Element of system_left_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
reconsider R1 = B2 as Relation of the carrier of TG ;
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, 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: (a ") * b in AB by 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: (c ") * d in AB by A26;
A32: ( z = c & y = d ) by A30, XTUPLE_0:1;
A33: ((a ") * b) * ((c ") * d) = (x ") * (z * ((z ") * y)) by A29, A32, GROUP_1:def 3
.= (x ") * ((z * (z ")) * y) by GROUP_1:def 3
.= (x ") * ((1_ TG) * y) by GROUP_1:def 5
.= (x ") * y by GROUP_1:def 4 ;
((a ") * b) * ((c ") * d) in AB * AB by A31, A28;
then (x ") * y in U by A18, A33, A17bis;
hence t in B1 by A17, A23; :: thesis: verum

end;

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

end;

hence system_left_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_left_uniformity TG).] ) by Th7;
hence UniformSpaceStr(# the carrier of TG,<.(system_left_uniformity TG).] #) is non empty UniformSpace ; :: thesis: verum