{} in {{}}
by TARSKI:def 1;
then reconsider r = {[{},{}]} as Relation of {{}} by RELSET_1:3;
set R = RelStr(# {{}},r #);
A2:
RelStr(# {{}},r #) is transitive
by A1;
RelStr(# {{}},r #) is directed
then reconsider R = RelStr(# {{}},r #) as non empty transitive directed RelStr by A2;
set V = the_universe_of the carrier of X;
set q = the Element of X;
set N = ConstantNet (R, the Element of X);
( RelStr(# the carrier of (ConstantNet (R, the Element of X)), the InternalRel of (ConstantNet (R, the Element of X)) #) = RelStr(# the carrier of R, the InternalRel of R #) & {} in the_universe_of the carrier of X )
by Def5, CLASSES2:56;
then
the carrier of (ConstantNet (R, the Element of X)) in the_universe_of the carrier of X
by CLASSES2:2;
hence
not NetUniv X is empty
by Def11; verum