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:99;
assume m < n ; :: thesis: m in dom (Directed (I,l))
then m in dom I by A1, AFINSQ_1:def 12;
hence m in dom (Directed (I,l)) by FUNCT_4:99; :: thesis: verum

end;

hence Directed (I,l) is initial by AFINSQ_1:def 12; :: thesis: verum