set V = the_universe_of the carrier of X;
{} in {{} } by TARSKI:def 1;
then reconsider r = {[{} ,{} ]} as Relation of {{} } by RELSET_1:8;
set R = RelStr(# {{} },r #);

A1: now

let x, y be Element of RelStr(# {{} },r #); :: thesis: x <= y
( x = {} & y = {} ) by TARSKI:def 1;
then [x,y] in {[{} ,{} ]} by TARSKI:def 1;
hence x <= y by ORDERS_2:def 9; :: thesis: verum

end;

A2: RelStr(# {{} },r #) is transitive

proof

let x, y, z be Element of RelStr(# {{} },r #); :: according to YELLOW_0:def 2 :: thesis: ( not x <= y or not y <= z or x <= z )
thus ( not x <= y or not y <= z or x <= z ) by A1; :: thesis: verum

end;

RelStr(# {{} },r #) is directed

proof

let x, y be Element of RelStr(# {{} },r #); :: according to YELLOW_6:def 5 :: thesis: ex z being Element of RelStr(# {{} },r #) st
( x <= z & y <= z )
take x ; :: thesis: ( x <= x & y <= x )
thus ( x <= x & y <= x ) by A1; :: thesis: verum

end;

then reconsider R = RelStr(# {{} },r #) as non empty transitive directed RelStr by A2;
consider q being Element of X;
set N = R --> q;
A3: RelStr(# the carrier of (R --> q),the InternalRel of (R --> q) #) = RelStr(# the carrier of R,the InternalRel of R #) by Def7;
{} in the_universe_of the carrier of X by CLASSES2:62;
then the carrier of (R --> q) in the_universe_of the carrier of X by A3, CLASSES2:3;
hence not NetUniv X is empty by Def14; :: thesis: verum