let m be Element of NAT ; :: thesis: not SubstPoset NAT ,{m} is complete
reconsider Cos = {(PFArt 1,m)} as Element of by Th31;
assume SubstPoset NAT ,{m} is complete ; :: thesis: contradiction
then consider a being Element of such that
A1: PFDrt m is_>=_than a and
A2: for b being Element of 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 a' = a as Element of Fin (PFuncs NAT ,{m}) ;
set Mi = Involved a';
PFDrt m is_>=_than Cos

proof

let u be Element of ; :: 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 empty Element of NAT such that
A3: u = PFBrt n1,m by Def5;

now

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 Th15; :: thesis: verum

end;

then a <> {} by A2, Th42;
then reconsider Mi = Involved a' as non empty finite Subset of by A1, Th37, Th43;
reconsider mX = (max Mi) + 1 as non empty Element of NAT ;
reconsider Sum = {(PFArt mX,m)} as Element of by Th31;
set b = a "\/" Sum;
Sum is_<=_than PFDrt m

proof

let t be Element of ; :: 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 empty 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 Th15; :: thesis: verum

end;

then A10: PFDrt m is_>=_than a "\/" Sum by A1, Th34;
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, Th15;

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, Th33;

now

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

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

hence contradiction by A17, ZFMISC_1:33; :: thesis: verum

end;

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

hence contradiction by A14, A16, Th38, XREAL_1:157; :: 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 by Th28;
PFBrt 1,m in PFDrt m by Def5;
then A19: P1 >= a "\/" Sum by A10, LATTICE3:def 8;
PFBrt 1,m <> {{} } by Th30;
hence contradiction by A13, A14, A18, A19, Th35, Th41; :: thesis: verum

end;

end;

end;

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