let QU be non void Quasi-UniformSpace; :: thesis: [: the carrier of QU, the carrier of QU:] in the entourages of QU
A1: not QU is void ;
set U = the Element of the entourages of QU;
the Element of the entourages of QU in the entourages of QU by A1;
then reconsider U = the Element of the entourages of QU as Subset of [: the carrier of QU, the carrier of QU:] ;
QU is upper ;
then A2: the entourages of QU is upper ;
[: the carrier of QU, the carrier of QU:] c= [: the carrier of QU, the carrier of QU:] ;
then reconsider Y = [: the carrier of QU, the carrier of QU:] as Subset of [: the carrier of QU, the carrier of QU:] ;
not the entourages of QU is empty by A1;
then Y in the entourages of QU by A2;
hence [: the carrier of QU, the carrier of QU:] in the entourages of QU ; :: thesis: verum