let USS be upper UniformSpaceStr ; :: thesis: ( meet the entourages of USS in the entourages of USS implies ex R being Relation of the carrier of USS st
( meet the entourages of USS = R & the entourages of USS = rho R ) )
assume A1: meet the entourages of USS in the entourages of USS ; :: thesis: ex R being Relation of the carrier of USS st
( meet the entourages of USS = R & the entourages of USS = rho R )
reconsider R = meet the entourages of USS as Relation of the carrier of USS ;
take R ; :: thesis: ( meet the entourages of USS = R & the entourages of USS = rho R )
A2: rho R c= the entourages of USS
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rho R or x in the entourages of USS )
assume x in rho R ; :: thesis: x in the entourages of USS
then consider S being Subset of [: the carrier of USS, the carrier of USS:] such that
A3: x = S and
A4: R c= S ;
the entourages of USS is upper by UNIFORM2:def 7;
hence x in the entourages of USS by A1, A3, A4; :: thesis: verum
end;
the entourages of USS c= rho R
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the entourages of USS or x in rho R )
assume x in the entourages of USS ; :: thesis: x in rho R
then consider S being Subset of [: the carrier of USS, the carrier of USS:] such that
A5: x = S and
A6: S in the entourages of USS ;
R c= S by A6, SETFAM_1:3;
hence x in rho R by A5; :: thesis: verum
end;
hence ( meet the entourages of USS = R & the entourages of USS = rho R ) by A2; :: thesis: verum