let m be Element of NAT ; :: thesis:
reconsider Cos = {(PFArt (1,m))} as Element of (SubstPoset (NAT,{m})) by Th28;
assume SubstPoset (NAT,{m}) is complete ; :: thesis:
then consider a being Element of (SubstPoset (NAT,{m})) such that
A1: PFDrt m is_>=_than a and
A2: for b being Element of (SubstPoset (NAT,{m})) st PFDrt m is_>=_than b holds
a >= b by LATTICE5:def 2;
SubstitutionSet (NAT,{m}) = the carrier of (SubstPoset (NAT,{m})) by SUBSTLAT:def 4;
then a in SubstitutionSet (NAT,{m}) ;
then reconsider a9 = a as Element of Fin (PFuncs (NAT,{m})) ;
set Mi = Involved a9;
PFDrt m is_>=_than Cos

let u be Element of (SubstPoset (NAT,{m})); :: according to LATTICE3:def 8 :: thesis:
assume u in PFDrt m ; :: thesis:
then consider n1 being non zero Element of NAT such that
A3: u = PFBrt (n1,m) by Def5;

let d be set ; :: thesis:
assume d in Cos ; :: thesis:
then A4: d = PFArt (1,m) by TARSKI:def 1;
1 <= n1 by NAT_1:14;
then d in PFBrt (n1,m) by A4, Def4;
hence ex e being set st
( e in u & e c= d ) by A3; :: thesis:

end;

hence Cos <= u by Th12; :: thesis:

end;

then a <> {} by A2, Th39;
then reconsider Mi = Involved a9 as non empty finite Subset of NAT by A1, Th34, Th40;
reconsider mX = (max Mi) + 1 as non zero Element of NAT ;
reconsider Sum = {(PFArt (mX,m))} as Element of (SubstPoset (NAT,{m})) by Th28;
set b = a "\/" Sum;
Sum is_<=_than PFDrt m

let t be Element of (SubstPoset (NAT,{m})); :: according to LATTICE3:def 8 :: thesis:
assume t in PFDrt m ; :: thesis:
then consider n being non zero Element of NAT such that
A5: t = PFBrt (n,m) by Def5;
for x being set st x in Sum holds
ex y being set st
( y in t & y c= x )

let x be set ; :: thesis:
assume A6: x in Sum ; :: thesis:
then A7: x = PFArt (mX,m) by TARSKI:def 1;

suppose A8: n < mX ; :: thesis:

take y = PFCrt (n,m); :: thesis:
thus y in t by A5, Def4; :: thesis:
thus y c= x by A7, A8, Lm7; :: thesis:

end;

suppose A9: n >= mX ; :: thesis:

take y = PFArt (mX,m); :: thesis:
thus y in t by A5, A9, Def4; :: thesis:
thus y c= x by A6, TARSKI:def 1; :: thesis:

end;

end;

end;

hence Sum <= t by Th12; :: thesis:

end;

then A10: PFDrt m is_>=_than a "\/" Sum by A1, Th31;
A11: a <> a "\/" Sum

A12: PFArt (mX,m) in Sum by TARSKI:def 1;
assume A13: a = a "\/" Sum ; :: thesis:
then Sum <= a by YELLOW_0:24;
then consider g being set such that
A14: g in a and
A15: g c= PFArt (mX,m) by A12, Th12;

suppose not g is empty ; :: thesis:

then consider n being Element of NAT such that
A16: [n,m] in g and
A17: n is even by A1, A14, Th30;

per cases by A15, A16, Def2;

suppose ex m9 being odd Element of NAT st
( m9 <= 2 * mX & [m9,m] = [n,m] ) ; :: thesis:

hence contradiction by A17, XTUPLE_0:1; :: thesis:

end;

suppose [(2 * mX),m] = [n,m] ; :: thesis:

hence contradiction by A14, A16, Th35, XREAL_1:155; :: thesis:

end;

end;

end;

hence contradiction ; :: thesis:

end;

suppose A18: g is empty ; :: thesis:

reconsider P1 = PFBrt (1,m) as Element of (SubstPoset (NAT,{m})) by Th25;
PFBrt (1,m) in PFDrt m by Def5;
then A19: P1 >= a "\/" Sum by A10;
PFBrt (1,m) <> {{}} by Th27;
hence contradiction by A13, A14, A18, A19, Th32, Th38; :: thesis:

end;

end;

end;

a <= a "\/" Sum by YELLOW_0:22;
then a < a "\/" Sum by A11, ORDERS_2:def 6;
hence contradiction by A2, A10, ORDERS_2:6; :: thesis: