let US be non void UniformSpaceStr ; :: thesis: ( ( for S being Element of the entourages of US ex R being Tolerance of the carrier of US st S = R ) implies ( US is axiom_U1 & US is axiom_U2 ) )
assume A2: for S being Element of the entourages of US ex R being Tolerance of the carrier of US st S = R ; :: thesis: ( US is axiom_U1 & US is axiom_U2 )
for S being Element of the entourages of US ex R being total reflexive Relation of the carrier of US st R = S
proof
let S be Element of the entourages of US; :: thesis: ex R being total reflexive Relation of the carrier of US st R = S
ex R being Tolerance of the carrier of US st R = S by A2;
hence ex R being total reflexive Relation of the carrier of US st R = S ; :: thesis: verum
end;
hence US is axiom_U1 by Th8; :: thesis: US is axiom_U2
for S being Element of the entourages of US ex R being Relation of the carrier of US st
( S = R & R is symmetric )
proof
let S be Element of the entourages of US; :: thesis: ex R being Relation of the carrier of US st
( S = R & R is symmetric )
ex R being Tolerance of the carrier of US st S = R by A2;
hence ex R being Relation of the carrier of US st
( S = R & R is symmetric ) ; :: thesis: verum
end;
hence US is axiom_U2 by Th10; :: thesis: verum