thus Directed I is initial :: thesis: not Directed I is empty

proof

let m, n be Nat; :: according to AFINSQ_1:def 12 :: thesis: ( not n in dom (Directed I) or n <= m or m in dom (Directed I) )
assume that
A1: n in dom (Directed I) and
A2: m < n ; :: thesis: m in dom (Directed I)
n in dom I by A1, FUNCT_4:99;
then m in dom I by A2, AFINSQ_1:def 12;
hence m in dom (Directed I) by FUNCT_4:99; :: thesis: verum

end;

thus not Directed I is empty ; :: thesis: verum