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 & n is even )
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 & n is even ) )
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 & n is even )
let X be non empty set ; :: thesis: ( X in a implies ex n being Element of NAT st
( [n,m] in X & n is even ) )
assume A2: X in a ; :: thesis: ex n being Element of NAT st
( [n,m] in X & n is even )
then reconsider X9 = X as non empty finite Subset of [:NAT,{m}:] by Th32;
assume A3: for n being Element of NAT st [n,m] in X holds
not n is even ; :: thesis: contradiction

A4: now

let k be non empty Element of NAT ; :: thesis: [((2 * k) + 1),m] in X
reconsider Pk = PFBrt (k,m) as Element of (SubstPoset (NAT,{m})) by Th28;
A5: [((2 * k) + 1),m] in PFCrt (k,m) by Def3;
Pk in PFDrt m by Def5;
then a <= Pk by A1, LATTICE3:def 8;
then consider y being set such that
A6: y in Pk and
A7: y c= X by A2, Th15;
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 empty 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 empty Element of NAT holds [((2 * l) + 1),m] in X9 by Th6;
hence contradiction by A4; :: thesis: verum