now

let m, n be Nat; :: thesis: ( n in dom (Directed I,l) & m < n implies m in dom (Directed I,l) )
assume n in dom (Directed I,l) ; :: thesis: ( m < n implies m in dom (Directed I,l) )
then A1: n in dom I by FUNCT_4:105;
assume m < n ; :: thesis: m in dom (Directed I,l)
then m in dom I by A1, AFINSQ_1:def 13;
hence m in dom (Directed I,l) by FUNCT_4:105; :: thesis: verum

end;

hence Directed I,l is initial by AFINSQ_1:def 13; :: thesis: verum