let QUS be Quasi-UniformSpace; :: thesis: ( the entourages of QUS is empty implies the entourages of (QUS [~]) = {{}} )
assume A1: the entourages of QUS is empty ; :: thesis: the entourages of (QUS [~]) = {{}}
reconsider EQUS = the entourages of QUS as Subset-Family of [: the carrier of QUS, the carrier of QUS:] ;
set X = { (U ~) where U is Element of the entourages of QUS : verum } ;
{ (U ~) where U is Element of the entourages of QUS : verum } = {{}}

proof

thus { (U ~) where U is Element of the entourages of QUS : verum } c= {{}} :: according to XBOOLE_0:def 10 :: thesis: {{}} c= { (U ~) where U is Element of the entourages of QUS : verum }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (U ~) where U is Element of the entourages of QUS : verum } or x in {{}} )
assume x in { (U ~) where U is Element of the entourages of QUS : verum } ; :: thesis: x in {{}}
then consider U being Element of the entourages of QUS such that
A11: x = U ~ ;
U = {} by A1, SUBSET_1:def 1;
then x = {} by A11;
hence x in {{}} by TARSKI:def 1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {{}} or x in { (U ~) where U is Element of the entourages of QUS : verum } )
assume x in {{}} ; :: thesis: x in { (U ~) where U is Element of the entourages of QUS : verum }
then A14: x = {} by TARSKI:def 1;
then reconsider y = x as Element of the entourages of QUS by A1, SUBSET_1:def 1;
y ~ = {} by A14;
hence x in { (U ~) where U is Element of the entourages of QUS : verum } by A14; :: thesis: verum

end;

hence the entourages of (QUS [~]) = {{}} ; :: thesis: verum