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 X' = 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;
Pk in PFDrt m by Def5;
then a <= Pk by A1, LATTICE3:def 8;
then consider y being set such that
A5: ( y in Pk & y c= X ) by A2, Th15;
A6: ( ex m' being non empty Element of NAT st
( m' <= k & y = PFArt m',m ) or y = PFCrt k,m ) by A5, Def4;
A7: for m' being Element of NAT holds
( not m' <= k or not y = PFArt m',m )

proof

given m' being Element of NAT such that A8: ( m' <= k & y = PFArt m',m ) ; :: thesis: contradiction
[(2 * m'),m] in PFArt m',m by Def2;
hence contradiction by A3, A5, A8; :: thesis: verum

end;

[((2 * k) + 1),m] in PFCrt k,m by Def3;
hence [((2 * k) + 1),m] in X by A5, A6, A7; :: thesis: verum

end;

consider l being non empty Element of NAT such that
A9: not [((2 * l) + 1),m] in X' by Th6;
thus contradiction by A4, A9; :: thesis: verum