let m, n be Nat; :: thesis: ( Domin_0 (n,m) is empty iff 2 * m > n )
thus ( Domin_0 (n,m) is empty implies 2 * m > n ) :: thesis: ( 2 * m > n implies Domin_0 (n,m) is empty )

proof

set q = m --> 1;
assume A1: Domin_0 (n,m) is empty ; :: thesis: 2 * m > n
assume A2: 2 * m <= n ; :: thesis: contradiction
m <= m + m by NAT_1:12;
then reconsider nm = n - m as Nat by A2, NAT_1:21, XXREAL_0:2;
set p = nm --> 0;
(2 * m) - m <= nm by A2, XREAL_1:9;
then A3: (nm --> 0) ^ (m --> 1) is dominated_by_0 by Th5;
( dom ((nm --> 0) ^ (m --> 1)) = (len (nm --> 0)) + (len (m --> 1)) & dom (nm --> 0) = nm ) by AFINSQ_1:def 3;
then A4: dom ((nm --> 0) ^ (m --> 1)) = nm + m ;
A5: Sum ((nm --> 0) ^ (m --> 1)) = (Sum (nm --> 0)) + (Sum (m --> 1)) by AFINSQ_2:55;
( Sum (nm --> 0) = 0 * nm & Sum (m --> 1) = 1 * m ) by AFINSQ_2:58;
hence contradiction by A1, A5, A4, A3, Def2; :: thesis: verum

end;

assume A6: 2 * m > n ; :: thesis: Domin_0 (n,m) is empty
assume not Domin_0 (n,m) is empty ; :: thesis: contradiction
then consider x being object such that
A7: x in Domin_0 (n,m) ;
consider p being XFinSequence of NAT such that
p = x and
A8: p is dominated_by_0 and
A9: dom p = n and
A10: Sum p = m by A7, Def2;
p | n = p by A9;
hence contradiction by A6, A8, A10, Th2; :: thesis: verum