let m be Element of NAT ; :: thesis: not SubstPoset (NAT,{m}) is complete
reconsider Cos = {(PFArt (1,m))} as Element of (SubstPoset (NAT,{m})) by Th28;
assume SubstPoset (NAT,{m}) is complete ; :: thesis: contradiction
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

proof

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

now :: thesis: for d being set st d in Cos holds
ex e being set st
( e in u & e c= d )

let d be set ; :: thesis: ( d in Cos implies ex e being set st
( e in u & e c= d ) )
assume d in Cos ; :: thesis: ex e being set st
( e in u & e c= d )
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: verum

end;

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

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

proof

let t be Element of (SubstPoset (NAT,{m})); :: according to LATTICE3:def 8 :: thesis: ( not t in PFDrt m or Sum <= t )
assume t in PFDrt m ; :: thesis: Sum <= t
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 )

proof

let x be set ; :: thesis: ( x in Sum implies ex y being set st
( y in t & y c= x ) )
assume A6: x in Sum ; :: thesis: ex y being set st
( y in t & y c= x )
then A7: x = PFArt (mX,m) by TARSKI:def 1;

per cases ( n < mX or n >= mX ) ;

suppose A8: n < mX ; :: thesis: ex y being set st
( y in t & y c= x )

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

end;

suppose A9: n >= mX ; :: thesis: ex y being set st
( y in t & y c= x )

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

end;

end;

end;

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

end;

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

proof

A12: PFArt (mX,m) in Sum by TARSKI:def 1;
assume A13: a = a "\/" Sum ; :: thesis: contradiction
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;

per cases ( not g is empty or g is empty ) ;

suppose not g is empty ; :: thesis: contradiction

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

now :: thesis: contradiction

per cases ( ex m9 being odd Element of NAT st
( m9 <= 2 * mX & [m9,m] = [n,m] ) or [(2 * mX),m] = [n,m] ) by A15, A16, Def2;

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

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

end;

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

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

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

suppose A18: g is empty ; :: thesis: contradiction

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: verum

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: verum