let QUS be Quasi-UniformSpace; :: thesis: ( the entourages of (QUS [~]) = {{}} & the entourages of (QUS [~]) is upper implies the carrier of QUS is empty )
assume that
A1: the entourages of (QUS [~]) = {{}} and
A2: the entourages of (QUS [~]) is upper ; :: thesis: the carrier of QUS is empty
reconsider X = the carrier of QUS as set ;
[:X,X:] c= [: the carrier of (QUS [~]), the carrier of (QUS [~]):] ;
then reconsider XX = [:X,X:] as Subset of [: the carrier of (QUS [~]), the carrier of (QUS [~]):] ;
{} c= [: the carrier of (QUS [~]), the carrier of (QUS [~]):] ;
then reconsider Y = {} as Subset of [: the carrier of (QUS [~]), the carrier of (QUS [~]):] ;
( Y in the entourages of (QUS [~]) & Y c= XX ) by A1, TARSKI:def 1;
then XX in the entourages of (QUS [~]) by A2;
hence the carrier of QUS is empty by A1, TARSKI:def 1; :: thesis: verum