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