let m, n be Nat; :: according to SCMNORM:def 1 :: 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)
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) by FUNCT_4:105; :: thesis: verum