{} in {{}} by TARSKI:def 1;
then reconsider r = {[{},{}]} as Relation of {{}} by RELSET_1:3;
set R = RelStr(# {{}},r #);
A1: now :: thesis: for x, y being Element of RelStr(# {{}},r #) holds x <= y
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 5; :: thesis: verum
end;
A2: RelStr(# {{}},r #) is transitive by A1;
RelStr(# {{}},r #) is directed
proof
let x, y be Element of RelStr(# {{}},r #); :: according to YELLOW_6:def 3 :: 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;
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; :: thesis: verum