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