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_in the carrier of US ) ) 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_in the carrier of US ) ; :: thesis: US is axiom_U2
A1: not US is void ;
US is axiom_U2
proof
let S be Element of the entourages of US; :: according to UNIFORM2:def 10 :: thesis: S [~] in the entourages of US
consider R being Relation of the carrier of US such that
A3: S = R and
A4: R is_symmetric_in the carrier of US by A2;
thus S ~ in the entourages of US :: thesis: verum
proof
R ~ = R
proof
thus R ~ c= R :: according to XBOOLE_0:def 10 :: thesis: R c= R ~
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in R ~ or x in R )
assume A7: x in R ~ ; :: thesis: x in R
then consider a, b being object such that
A8: a in the carrier of US and
A9: b in the carrier of US and
A10: x = [a,b] by ZFMISC_1:def 2;
[b,a] in R by A7, A10, RELAT_1:def 7;
hence x in R by A10, A4, A8, A9, RELAT_2:def 3; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in R or x in R ~ )
assume A11: x in R ; :: thesis: x in R ~
then consider a, b being object such that
A12: a in the carrier of US and
A13: b in the carrier of US and
A14: x = [a,b] by ZFMISC_1:def 2;
[b,a] in R ~ by A11, A14, RELAT_1:def 7;
hence x in R ~ by Th4, A4, A12, A13, A14, RELAT_2:def 3; :: thesis: verum
end;
hence S ~ in the entourages of US by A1, A3; :: thesis: verum
end;
end;
hence US is axiom_U2 ; :: thesis: verum