now

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

end;

hence Directed I,l is initial by SCMNORM:def 1; :: thesis: verum