let US be UniformSpaceStr ; :: thesis: ( US is axiom_U2 implies for S being Element of the entourages of US
for x, y being Element of US st [x,y] in S holds
[y,x] in union the entourages of US )
assume A1: US is axiom_U2 ; :: thesis: for S being Element of the entourages of US
for x, y being Element of US st [x,y] in S holds
[y,x] in union the entourages of US
let S be Element of the entourages of US; :: thesis: for x, y being Element of US st [x,y] in S holds
[y,x] in union the entourages of US
let x, y be Element of US; :: thesis: ( [x,y] in S implies [y,x] in union the entourages of US )
assume A3: [x,y] in S ; :: thesis: [y,x] in union the entourages of US
reconsider SFX = the entourages of US as non empty Subset-Family of [: the carrier of US, the carrier of US:] by A1;
A6: [y,x] in S ~ by A3, RELAT_1:def 7;
S ~ in the entourages of US by A1;
hence [y,x] in union the entourages of US by A6, TARSKI:def 4; :: thesis: verum