let US be non void UniformSpaceStr ; :: thesis: ( US is axiom_U1 iff for S being Element of the entourages of US ex R being total reflexive Relation of the carrier of US st R = S )
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 total reflexive Relation of the carrier of US st R = S ) implies US is axiom_U1 )
assume A2: US is axiom_U1 ; :: thesis: for S being Element of the entourages of US ex R being total reflexive Relation of the carrier of US st R = S
hereby :: thesis: verum
let S be Element of the entourages of US; :: thesis: ex R being total reflexive Relation of the carrier of US st R = S
consider R being Relation of the carrier of US such that
A3: R = S and
A4: R is_reflexive_in the carrier of US by A2, Th7;
A5: field R = the carrier of US by A4, PARTIT_2:9;
reconsider R = R as total reflexive Relation of the carrier of US by A5, A4, TAXONOM1:3, PARTFUN1:def 2, RELAT_2:def 9;
take R = R; :: thesis: R = S
thus R = S by A3; :: thesis: verum
end;
end;
assume A6: for S being Element of the entourages of US ex R being total reflexive Relation of the carrier of US st R = S ; :: thesis: US is axiom_U1
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 )
consider R being total reflexive Relation of the carrier of US such that
A7: R = S by A6;
reconsider R = R as Relation of the carrier of US ;
take R = R; :: thesis: ( R = S & R is_reflexive_in the carrier of US )
thus R = S by A7; :: 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 A8: x in the carrier of US ; :: thesis: [x,x] in R
field R = the carrier of US by ORDERS_1:12;
hence [x,x] in R by A8, RELAT_2:def 9, RELAT_2:def 1; :: thesis: verum
end;
hence R is_reflexive_in the carrier of US by RELAT_2:def 1; :: thesis: verum
end;
hence US is axiom_U1 by Th7; :: thesis: verum