let m be Element of NAT ; :: thesis: for a being Element of (SubstPoset (NAT,{m})) st PFDrt m is_>=_than a holds
for X being non empty set st X in a holds
ex n being Element of NAT st
( [n,m] in X & not n is odd )
let a be Element of (SubstPoset (NAT,{m})); :: thesis: ( PFDrt m is_>=_than a implies for X being non empty set st X in a holds
ex n being Element of NAT st
( [n,m] in X & not n is odd ) )
assume A1: PFDrt m is_>=_than a ; :: thesis: for X being non empty set st X in a holds
ex n being Element of NAT st
( [n,m] in X & not n is odd )
let X be non empty set ; :: thesis: ( X in a implies ex n being Element of NAT st
( [n,m] in X & not n is odd ) )
assume A2: X in a ; :: thesis: ex n being Element of NAT st
( [n,m] in X & not n is odd )
then reconsider X9 = X as non empty finite Subset of [:NAT,{m}:] by Th29;
assume A3: for n being Element of NAT st [n,m] in X holds
n is odd ; :: thesis: contradiction

A4: now :: thesis: for k being non zero Element of NAT holds [((2 * k) + 1),m] in X

let k be non zero Element of NAT ; :: thesis: [((2 * k) + 1),m] in X
reconsider Pk = PFBrt (k,m) as Element of (SubstPoset (NAT,{m})) by Th25;
A5: [((2 * k) + 1),m] in PFCrt (k,m) by Def3;
Pk in PFDrt m by Def5;
then a <= Pk by A1;
then consider y being set such that
A6: y in Pk and
A7: y c= X by A2, Th12;
A8: for m9 being Element of NAT holds
( not m9 <= k or not y = PFArt (m9,m) )

proof

given m9 being Element of NAT such that m9 <= k and
A9: y = PFArt (m9,m) ; :: thesis: contradiction
[(2 * m9),m] in PFArt (m9,m) by Def2;
hence contradiction by A3, A7, A9; :: thesis: verum

end;

( ex m9 being non zero Element of NAT st
( m9 <= k & y = PFArt (m9,m) ) or y = PFCrt (k,m) ) by A6, Def4;
hence [((2 * k) + 1),m] in X by A7, A8, A5; :: thesis: verum

end;

not for l being non zero Element of NAT holds [((2 * l) + 1),m] in X9 by Th4;
hence contradiction by A4; :: thesis: verum