let US be non void UniformSpaceStr ; :: thesis: ( ( for S being Element of the entourages of US ex R being Relation of the carrier of US st
( S = R & R is symmetric ) ) implies US is axiom_U2 )
assume A2: for S being Element of the entourages of US ex R being Relation of the carrier of US st
( S = R & R is symmetric ) ; :: thesis: US is axiom_U2
now :: thesis: for S being Element of the entourages of US ex R being Relation of the carrier of US st
( S = R & R is_symmetric_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
( S = R & R is_symmetric_in the carrier of US )
consider R being Relation of the carrier of US such that
B1: S = R and
B2: R is symmetric by A2;
take R = R; :: thesis: ( S = R & R is_symmetric_in the carrier of US )
thus S = R by B1; :: thesis: R is_symmetric_in the carrier of US
for x, y being object st x in the carrier of US & y in the carrier of US & [x,y] in R holds
[y,x] in R by B2, PREFER_1:20;
hence R is_symmetric_in the carrier of US by RELAT_2:def 3; :: thesis: verum
end;
hence US is axiom_U2 by Th9; :: thesis: verum