let US be non void UniformSpaceStr ; :: thesis: ( US is axiom_U1 iff for S being Element of the entourages of US ex R being Relation of the carrier of US st
( R = S & R is_reflexive_in the carrier of US ) )
not US is void ;
then reconsider SFX = the entourages of US as non empty Subset-Family of [: the carrier of US, the carrier of US:] ;
hereby :: thesis: ( ( for S being Element of the entourages of US ex R being Relation of the carrier of US st
( R = S & R is_reflexive_in the carrier of US ) ) implies US is axiom_U1 )
assume A1: US is axiom_U1 ; :: thesis: for S being Element of the entourages of US ex R being Relation of the carrier of US st
( R = S & R is_reflexive_in the carrier of US )
now :: thesis: for S being Element of the entourages of US ex R being Relation of the carrier of US st
( R = S & R is_reflexive_in the carrier of US )
let S be Element of the entourages of US; :: thesis: ex R being Relation of the carrier of US st
( R = S & R is_reflexive_in the carrier of US )
S is Element of SFX ;
then consider R being Relation of the carrier of US such that
A2: R = S ;
take R = R; :: thesis: ( R = S & R is_reflexive_in the carrier of US )
thus R = S by A2; :: thesis: R is_reflexive_in the carrier of US
now :: thesis: for x being object st x in the carrier of US holds
[x,x] in R
let x be object ; :: thesis: ( x in the carrier of US implies [x,x] in R )
assume x in the carrier of US ; :: thesis: [x,x] in R
then A3: [x,x] in id the carrier of US by RELAT_1:def 10;
id the carrier of US c= S by A1;
hence [x,x] in R by A3, A2; :: thesis: verum
end;
hence R is_reflexive_in the carrier of US by RELAT_2:def 1; :: thesis: verum
end;
hence for S being Element of the entourages of US ex R being Relation of the carrier of US st
( R = S & R is_reflexive_in the carrier of US ) ; :: thesis: verum
end;
assume A4: for S being Element of the entourages of US ex R being Relation of the carrier of US st
( R = S & R is_reflexive_in the carrier of US ) ; :: thesis: US is axiom_U1
now :: thesis: for S being Element of the entourages of US holds id the carrier of US c= S
let S be Element of the entourages of US; :: thesis: id the carrier of US c= S
consider R being Relation of the carrier of US such that
A5: R = S and
A6: R is_reflexive_in the carrier of US by A4;
for x being object st x in the carrier of US holds
[x,x] in R by A6, RELAT_2:def 1;
hence id the carrier of US c= S by A5, RELAT_1:47; :: thesis: verum
end;
hence US is axiom_U1 ; :: thesis: verum