:: HEYTING3 semantic presentation

begin

scheme :: HEYTING3:sch 1
SSubsetUniq{ F1() ->  1-sorted , P1[ set ] } :
 for A1, A2 being Subset of F1() st ( for x being set holds
( x in A1 iff P1[x] ) ) & ( for x being set holds
( x in A2 iff P1[x] ) ) holds
A1 = A2
proof
let A1, A2 be Subset of F1(); ::_thesis: ( ( for x being set holds
( x in A1 iff P1[x] ) ) & ( for x being set holds
( x in A2 iff P1[x] ) ) implies A1 = A2 )
assume that
A1: for x being set holds
( x in A1 iff P1[x] ) and
A2: for x being set holds
( x in A2 iff P1[x] ) ; ::_thesis: A1 = A2
thus  A1 c= A2 :: according to XBOOLE_0:def_10 ::_thesis: A2 c= A1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A1 or x in A2 )
assume  x in A1 ; ::_thesis: x in A2
then  P1[x] by A1;
hence  x in A2 by A2; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A2 or x in A1 )
assume  x in A2 ; ::_thesis: x in A1
then  P1[x] by A2;
hence  x in A1 by A1; ::_thesis: verum
end;

Lm1:  for A, x being set holds [:A,{x}:] is Function
proof
let A, x be set ; ::_thesis: [:A,{x}:] is Function
set X = [:A,{x}:];
 [:A,{x}:] is Function-like
proof
let y, y1, y2 be set ; :: according to FUNCT_1:def_1 ::_thesis: ( not [y,y1] in [:A,{x}:] or not [y,y2] in [:A,{x}:] or y1 = y2 )
assume that
A1: [y,y1] in [:A,{x}:] and
A2: [y,y2] in [:A,{x}:] ; ::_thesis: y1 = y2
 y1 = x by A1, ZFMISC_1:106;
hence  y1 = y2 by A2, ZFMISC_1:106; ::_thesis: verum
end;
hence  [:A,{x}:] is Function ; ::_thesis: verum
end;

registration
let A, x be set ;
cluster[:A,{x}:] ->  Function-like ;
coherence
 [:A,{x}:] is Function-like by Lm1;
end;

Lm2:  0 = 2 * 0
;

Lm3:  1 = 0 + 1
;

theorem Th1: :: HEYTING3:1
for X being non empty finite Subset of NAT ex n being Element of NAT st X c= (Seg n) \/ {0}
proof
let X be non empty finite Subset of NAT; ::_thesis: ex n being Element of NAT st X c= (Seg n) \/ {0}
reconsider m = max X as Element of NAT by ORDINAL1:def_12;
take  m ; ::_thesis: X c= (Seg m) \/ {0}
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in (Seg m) \/ {0} )
A1: Seg m c= (Seg m) \/ {0} by XBOOLE_1:7;
A2: {0} c= (Seg m) \/ {0} by XBOOLE_1:7;
assume A3: x in X ; ::_thesis: x in (Seg m) \/ {0}
then reconsider n = x as Element of NAT ;
A4: n <= m by A3, XXREAL_2:def_8;
percases ( 1 <= n or 0 = n ) by NAT_1:25;
suppose 1 <= n ; ::_thesis: x in (Seg m) \/ {0}
then  n in Seg m by A4, FINSEQ_1:1;
hence  x in (Seg m) \/ {0} by A1; ::_thesis: verum
end;
suppose 0 = n ; ::_thesis: x in (Seg m) \/ {0}
then  n in {0} by TARSKI:def_1;
hence  x in (Seg m) \/ {0} by A2; ::_thesis: verum
end;
end;
end;

theorem :: HEYTING3:2
for X being finite Subset of NAT holds
not for k being odd Element of NAT holds k in X
proof
let X be finite Subset of NAT; ::_thesis: not for k being odd Element of NAT holds k in X
percases ( not X is empty or X is empty ) ;
suppose not X is empty ; ::_thesis: not for k being odd Element of NAT holds k in X
then consider n being Element of NAT  such that
A1: X c= (Seg n) \/ {0} by Th1;
A2: not (2 * n) + 1 in X
proof
A3: not (2 * n) + 1 in {0} by TARSKI:def_1;
assume  (2 * n) + 1 in X ; ::_thesis: contradiction
then  (2 * n) + 1 in Seg n by A1, A3, XBOOLE_0:def_3;
then A4: (2 * n) + 1 <= n by FINSEQ_1:1;
 1 * n <= 2 * n by NAT_1:4;
hence  contradiction by A4, NAT_1:13; ::_thesis: verum
end;
assume  for k being odd Element of NAT holds k in X ; ::_thesis: contradiction
hence  contradiction by A2; ::_thesis: verum
end;
suppose X is empty ; ::_thesis: not for k being odd Element of NAT holds k in X
hence  not for k being odd Element of NAT holds k in X ; ::_thesis: verum
end;
end;
end;

theorem Th3: :: HEYTING3:3
for k being Element of NAT
for X being non empty finite Subset of [:NAT,{k}:] ex n being non empty Element of NAT st X c= [:((Seg n) \/ {0}),{k}:]
proof
let k be Element of NAT ; ::_thesis: for X being non empty finite Subset of [:NAT,{k}:] ex n being non empty Element of NAT st X c= [:((Seg n) \/ {0}),{k}:]
let X be non empty finite Subset of [:NAT,{k}:]; ::_thesis: ex n being non empty Element of NAT st X c= [:((Seg n) \/ {0}),{k}:]
reconsider pX = proj1 X as non empty finite Subset of NAT by FUNCT_5:11;
reconsider mpX = max pX as Element of NAT by ORDINAL1:def_12;
reconsider m = mpX + 1 as non empty Element of NAT ;
take  m ; ::_thesis: X c= [:((Seg m) \/ {0}),{k}:]
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in [:((Seg m) \/ {0}),{k}:] )
A1: Seg m c= (Seg m) \/ {0} by XBOOLE_1:7;
A2: {0} c= (Seg m) \/ {0} by XBOOLE_1:7;
assume A3: x in X ; ::_thesis: x in [:((Seg m) \/ {0}),{k}:]
then consider x1, x2 being set  such that
A4: x1 in NAT and
A5: x2 in {k} and
A6: x = [x1,x2] by ZFMISC_1:def_2;
reconsider n = x `1 as Element of NAT by A4, A6, MCART_1:7;
A7: x1 = x `1 by A6, MCART_1:7;
 [x1,x2] `1 = x1 ;
then  n in pX by A3, A6, XTUPLE_0:def_12;
then  ( max pX <= m & n <= max pX ) by NAT_1:11, XXREAL_2:def_8;
then A8: n <= m by XXREAL_0:2;
percases ( 1 <= n or 0 = n ) by NAT_1:25;
suppose 1 <= n ; ::_thesis: x in [:((Seg m) \/ {0}),{k}:]
then  n in Seg m by A8, FINSEQ_1:1;
hence  x in [:((Seg m) \/ {0}),{k}:] by A5, A6, A7, A1, ZFMISC_1:87; ::_thesis: verum
end;
suppose 0 = n ; ::_thesis: x in [:((Seg m) \/ {0}),{k}:]
then  n in {0} by TARSKI:def_1;
hence  x in [:((Seg m) \/ {0}),{k}:] by A5, A6, A7, A2, ZFMISC_1:87; ::_thesis: verum
end;
end;
end;

theorem Th4: :: HEYTING3:4
for m being Element of NAT
for X being non empty finite Subset of [:NAT,{m}:] holds
not for k being non empty Element of NAT holds [((2 * k) + 1),m] in X
proof
let m be Element of NAT ; ::_thesis: for X being non empty finite Subset of [:NAT,{m}:] holds
not for k being non empty Element of NAT holds [((2 * k) + 1),m] in X
let X be non empty finite Subset of [:NAT,{m}:]; ::_thesis: not for k being non empty Element of NAT holds [((2 * k) + 1),m] in X
consider n being non empty Element of NAT  such that
A1: X c= [:((Seg n) \/ {0}),{m}:] by Th3;
A2: not [((2 * n) + 1),m] in X
proof
assume  [((2 * n) + 1),m] in X ; ::_thesis: contradiction
then A3: (2 * n) + 1 in (Seg n) \/ {0} by A1, ZFMISC_1:87;
 not (2 * n) + 1 in {0} by TARSKI:def_1;
then  (2 * n) + 1 in Seg n by A3, XBOOLE_0:def_3;
then A4: (2 * n) + 1 <= n by FINSEQ_1:1;
 1 * n <= 2 * n by NAT_1:4;
hence  contradiction by A4, NAT_1:13; ::_thesis: verum
end;
assume  for k being non empty Element of NAT holds [((2 * k) + 1),m] in X ; ::_thesis: contradiction
hence  contradiction by A2; ::_thesis: verum
end;

theorem :: HEYTING3:5
for m being Element of NAT
for X being finite Subset of [:NAT,{m}:] ex k being Element of NAT st
for l being Element of NAT st l >= k holds
not [l,m] in X
proof
let m be Element of NAT ; ::_thesis: for X being finite Subset of [:NAT,{m}:] ex k being Element of NAT st
for l being Element of NAT st l >= k holds
not [l,m] in X
let X be finite Subset of [:NAT,{m}:]; ::_thesis: ex k being Element of NAT st
for l being Element of NAT st l >= k holds
not [l,m] in X
percases ( not X is empty or X is empty ) ;
suppose not X is empty ; ::_thesis: ex k being Element of NAT st
for l being Element of NAT st l >= k holds
not [l,m] in X
then reconsider X9 = X as non empty finite Subset of [:NAT,{m}:] ;
consider n being non empty Element of NAT  such that
A1: X9 c= [:((Seg n) \/ {0}),{m}:] by Th3;
take k = n + 1; ::_thesis: for l being Element of NAT st l >= k holds
not [l,m] in X
let l be Element of NAT ; ::_thesis: ( l >= k implies not [l,m] in X )
assume A2: l >= k ; ::_thesis: not [l,m] in X
assume  [l,m] in X ; ::_thesis: contradiction
then A3: l in (Seg n) \/ {0} by A1, ZFMISC_1:87;
now__::_thesis:_contradiction
percases ( l in Seg n or l in {0} ) by A3, XBOOLE_0:def_3;
suppose l in Seg n ; ::_thesis: contradiction
then  l <= n by FINSEQ_1:1;
hence  contradiction by A2, NAT_1:13; ::_thesis: verum
end;
suppose l in {0} ; ::_thesis: contradiction
hence  contradiction by A2, TARSKI:def_1; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;
suppose X is empty ; ::_thesis: ex k being Element of NAT st
for l being Element of NAT st l >= k holds
not [l,m] in X
then  for l being Element of NAT st l >= 0 holds
not [l,m] in X ;
hence  ex k being Element of NAT st
for l being Element of NAT st l >= k holds
not [l,m] in X ; ::_thesis: verum
end;
end;
end;

theorem :: HEYTING3:6
for L being upper-bounded Lattice holds Top L = Top (LattPOSet L)
proof
let L be upper-bounded Lattice; ::_thesis: Top L = Top (LattPOSet L)
set x = % (Top (LattPOSet L));
now__::_thesis:_for_a_being_Element_of_L_holds_
(_(%_(Top_(LattPOSet_L)))_"\/"_a_=_%_(Top_(LattPOSet_L))_&_a_"\/"_(%_(Top_(LattPOSet_L)))_=_%_(Top_(LattPOSet_L))_)
let a be Element of L; ::_thesis: ( (% (Top (LattPOSet L))) "\/" a = % (Top (LattPOSet L)) & a "\/" (% (Top (LattPOSet L))) = % (Top (LattPOSet L)) )
 a % <= (% (Top (LattPOSet L))) % by YELLOW_0:45;
then  a [= % (Top (LattPOSet L)) by LATTICE3:7;
hence  ( (% (Top (LattPOSet L))) "\/" a = % (Top (LattPOSet L)) & a "\/" (% (Top (LattPOSet L))) = % (Top (LattPOSet L)) ) by LATTICES:def_3; ::_thesis: verum
end;
hence  Top L = Top (LattPOSet L) by LATTICES:def_17; ::_thesis: verum
end;

theorem :: HEYTING3:7
for L being lower-bounded Lattice holds Bottom L = Bottom (LattPOSet L)
proof
let L be lower-bounded Lattice; ::_thesis: Bottom L = Bottom (LattPOSet L)
set x = % (Bottom (LattPOSet L));
now__::_thesis:_for_a_being_Element_of_L_holds_
(_(%_(Bottom_(LattPOSet_L)))_"/\"_a_=_%_(Bottom_(LattPOSet_L))_&_a_"/\"_(%_(Bottom_(LattPOSet_L)))_=_%_(Bottom_(LattPOSet_L))_)
let a be Element of L; ::_thesis: ( (% (Bottom (LattPOSet L))) "/\" a = % (Bottom (LattPOSet L)) & a "/\" (% (Bottom (LattPOSet L))) = % (Bottom (LattPOSet L)) )
 a % >= (% (Bottom (LattPOSet L))) % by YELLOW_0:44;
then  % (Bottom (LattPOSet L)) [= a by LATTICE3:7;
hence  ( (% (Bottom (LattPOSet L))) "/\" a = % (Bottom (LattPOSet L)) & a "/\" (% (Bottom (LattPOSet L))) = % (Bottom (LattPOSet L)) ) by LATTICES:4; ::_thesis: verum
end;
hence  Bottom L = Bottom (LattPOSet L) by LATTICES:def_16; ::_thesis: verum
end;

begin

theorem :: HEYTING3:8
for V being set
for C being finite set
for A, B being Element of Fin (PFuncs (V,C)) st A = {} & B <> {} holds
B =>> A = {}
proof
let V be set ; ::_thesis: for C being finite set
for A, B being Element of Fin (PFuncs (V,C)) st A = {} & B <> {} holds
B =>> A = {}
let C be finite set ; ::_thesis: for A, B being Element of Fin (PFuncs (V,C)) st A = {} & B <> {} holds
B =>> A = {}
let A, B be Element of Fin (PFuncs (V,C)); ::_thesis: ( A = {} & B <> {} implies B =>> A = {} )
assume A1: ( A = {} & B <> {} ) ; ::_thesis: B =>> A = {}
assume  B =>> A <> {} ; ::_thesis: contradiction
then consider k being set  such that
A2: k in B =>> A by XBOOLE_0:def_1;
 ex f being PartFunc of B,A st
( k = union  {  ((f . i) \ i) where i is Element of PFuncs (V,C) : i in B  }  & dom f = B ) by A2, HEYTING2:15;
hence  contradiction by A1; ::_thesis: verum
end;

theorem Th9: :: HEYTING3:9
for V, V9, C, C9 being set st V c= V9 & C c= C9 holds
SubstitutionSet (V,C) c= SubstitutionSet (V9,C9)
proof
let V, V9, C, C9 be set ; ::_thesis: ( V c= V9 & C c= C9 implies SubstitutionSet (V,C) c= SubstitutionSet (V9,C9) )
assume  ( V c= V9 & C c= C9 ) ; ::_thesis: SubstitutionSet (V,C) c= SubstitutionSet (V9,C9)
then A1: PFuncs (V,C) c= PFuncs (V9,C9) by PARTFUN1:50;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in SubstitutionSet (V,C) or x in SubstitutionSet (V9,C9) )
assume  x in SubstitutionSet (V,C) ; ::_thesis: x in SubstitutionSet (V9,C9)
then  x in  {  A where A is Element of Fin (PFuncs (V,C)) : ( ( for u being set st u in A holds
u is finite ) & ( for s, t being Element of PFuncs (V,C) st s in A & t in A & s c= t holds
s = t ) )  }  by SUBSTLAT:def_1;
then consider B being Element of Fin (PFuncs (V,C)) such that
A2: ( B = x & ( for u being set st u in B holds
u is finite ) ) and
A3: for s, t being Element of PFuncs (V,C) st s in B & t in B & s c= t holds
s = t ;
A4: ( B in Fin (PFuncs (V,C)) & Fin (PFuncs (V,C)) c= Fin (PFuncs (V9,C9)) ) by A1, FINSUB_1:10;
A5: B c= PFuncs (V,C) by FINSUB_1:def_5;
reconsider B = B as Element of Fin (PFuncs (V9,C9)) by A4;
 for s, t being Element of PFuncs (V9,C9) st s in B & t in B & s c= t holds
s = t by A3, A5;
then  x in  {  D where D is Element of Fin (PFuncs (V9,C9)) : ( ( for u being set st u in D holds
u is finite ) & ( for s, t being Element of PFuncs (V9,C9) st s in D & t in D & s c= t holds
s = t ) )  }  by A2;
hence  x in SubstitutionSet (V9,C9) by SUBSTLAT:def_1; ::_thesis: verum
end;

theorem Th10: :: HEYTING3:10
for V, V9, C, C9 being set
for A being Element of Fin (PFuncs (V,C))
for B being Element of Fin (PFuncs (V9,C9)) st V c= V9 & C c= C9 & A = B holds
mi A = mi B
proof
let V, V9, C, C9 be set ; ::_thesis: for A being Element of Fin (PFuncs (V,C))
for B being Element of Fin (PFuncs (V9,C9)) st V c= V9 & C c= C9 & A = B holds
mi A = mi B
let A be Element of Fin (PFuncs (V,C)); ::_thesis: for B being Element of Fin (PFuncs (V9,C9)) st V c= V9 & C c= C9 & A = B holds
mi A = mi B
let B be Element of Fin (PFuncs (V9,C9)); ::_thesis: ( V c= V9 & C c= C9 & A = B implies mi A = mi B )
assume that
A1: ( V c= V9 & C c= C9 ) and
A2: A = B ; ::_thesis: mi A = mi B
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: mi B c= mi A
let x be set ; ::_thesis: ( x in mi A implies x in mi B )
A3: PFuncs (V,C) c= PFuncs (V9,C9) by A1, PARTFUN1:50;
assume A4: x in mi A ; ::_thesis: x in mi B
then  x in  {  t where t is Element of PFuncs (V,C) : ( t is finite & ( for s being Element of PFuncs (V,C) holds
( ( s in A & s c= t ) iff s = t ) ) )  }  by SUBSTLAT:def_2;
then consider f being Element of PFuncs (V,C) such that
A5: f = x and
A6: f is finite and
 for s being Element of PFuncs (V,C) holds
( ( s in A & s c= f ) iff s = f ) ;
 x in PFuncs (V,C) by A5;
then reconsider f = f as Element of PFuncs (V9,C9) by A5, A3;
 for s being Element of PFuncs (V9,C9) holds
( ( s in B & s c= f ) iff s = f ) by A2, A4, A5, SUBSTLAT:6;
then  x in  {  t where t is Element of PFuncs (V9,C9) : ( t is finite & ( for s being Element of PFuncs (V9,C9) holds
( ( s in B & s c= t ) iff s = t ) ) )  }  by A5, A6;
hence  x in mi B by SUBSTLAT:def_2; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in mi B or x in mi A )
assume A7: x in mi B ; ::_thesis: x in mi A
then  x in  {  t where t is Element of PFuncs (V9,C9) : ( t is finite & ( for s being Element of PFuncs (V9,C9) holds
( ( s in B & s c= t ) iff s = t ) ) )  }  by SUBSTLAT:def_2;
then  ex f being Element of PFuncs (V9,C9) st
( f = x & f is finite & ( for s being Element of PFuncs (V9,C9) holds
( ( s in B & s c= f ) iff s = f ) ) ) ;
then reconsider x9 = x as finite set ;
 ( mi B c= B & ( for b being finite set st b in A & b c= x9 holds
b = x9 ) ) by A2, A7, SUBSTLAT:6, SUBSTLAT:8;
hence  x in mi A by A2, A7, SUBSTLAT:7; ::_thesis: verum
end;

theorem :: HEYTING3:11
for V, V9, C, C9 being set st V c= V9 & C c= C9 holds
the L_join of (SubstLatt (V,C)) = the L_join of (SubstLatt (V9,C9)) || the carrier of (SubstLatt (V,C))
proof
let V, V9, C, C9 be set ; ::_thesis: ( V c= V9 & C c= C9 implies the L_join of (SubstLatt (V,C)) = the L_join of (SubstLatt (V9,C9)) || the carrier of (SubstLatt (V,C)) )
set K = SubstLatt (V,C);
set L = SubstLatt (V9,C9);
A1: SubstitutionSet (V,C) = the carrier of (SubstLatt (V,C)) by SUBSTLAT:def_4;
A2: dom the L_join of (SubstLatt (V9,C9)) = [: the carrier of (SubstLatt (V9,C9)), the carrier of (SubstLatt (V9,C9)):] by FUNCT_2:def_1;
reconsider B1 = the L_join of (SubstLatt (V,C)) as BinOp of the carrier of (SubstLatt (V,C)) ;
set B2 = the L_join of (SubstLatt (V9,C9)) || the carrier of (SubstLatt (V,C));
assume A3: ( V c= V9 & C c= C9 ) ; ::_thesis: the L_join of (SubstLatt (V,C)) = the L_join of (SubstLatt (V9,C9)) || the carrier of (SubstLatt (V,C))
 SubstitutionSet (V9,C9) = the carrier of (SubstLatt (V9,C9)) by SUBSTLAT:def_4;
then  the carrier of (SubstLatt (V,C)) c= the carrier of (SubstLatt (V9,C9)) by A1, A3, Th9;
then A4: dom ( the L_join of (SubstLatt (V9,C9)) || the carrier of (SubstLatt (V,C))) = [: the carrier of (SubstLatt (V,C)), the carrier of (SubstLatt (V,C)):] by A2, RELAT_1:62, ZFMISC_1:96;
A5: SubstitutionSet (V,C) c= SubstitutionSet (V9,C9) by A3, Th9;
 rng ( the L_join of (SubstLatt (V9,C9)) || the carrier of (SubstLatt (V,C))) c= the carrier of (SubstLatt (V,C))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng ( the L_join of (SubstLatt (V9,C9)) || the carrier of (SubstLatt (V,C))) or x in the carrier of (SubstLatt (V,C)) )
assume  x in rng ( the L_join of (SubstLatt (V9,C9)) || the carrier of (SubstLatt (V,C))) ; ::_thesis: x in the carrier of (SubstLatt (V,C))
then consider y being set  such that
A6: y in dom ( the L_join of (SubstLatt (V9,C9)) || the carrier of (SubstLatt (V,C))) and
A7: x = ( the L_join of (SubstLatt (V9,C9)) || the carrier of (SubstLatt (V,C))) . y by FUNCT_1:def_3;
consider y1, y2 being set  such that
A8: ( y1 in the carrier of (SubstLatt (V,C)) & y2 in the carrier of (SubstLatt (V,C)) ) and
A9: y = [y1,y2] by A4, A6, ZFMISC_1:def_2;
 ( y1 in SubstitutionSet (V,C) & y2 in SubstitutionSet (V,C) ) by A8, SUBSTLAT:def_4;
then reconsider y19 = y1, y29 = y2 as Element of SubstitutionSet (V9,C9) by A5;
reconsider y11 = y1, y22 = y2 as Element of SubstitutionSet (V,C) by A8, SUBSTLAT:def_4;
( the L_join of (SubstLatt (V9,C9)) || the carrier of (SubstLatt (V,C))) . y = the L_join of (SubstLatt (V9,C9)) . (y1,y2) by A4, A6, A9, FUNCT_1:49
.= mi (y19 \/ y29) by SUBSTLAT:def_4
.= mi (y11 \/ y22) by A3, Th10 ;
hence  x in the carrier of (SubstLatt (V,C)) by A1, A7; ::_thesis: verum
end;
then reconsider B2 = the L_join of (SubstLatt (V9,C9)) || the carrier of (SubstLatt (V,C)) as BinOp of the carrier of (SubstLatt (V,C)) by A4, FUNCT_2:2;
now__::_thesis:_for_a,_b_being_Element_of_(SubstLatt_(V,C))_holds_B1_._(a,b)_=_B2_._(a,b)
let a, b be Element of (SubstLatt (V,C)); ::_thesis: B1 . (a,b) = B2 . (a,b)
reconsider a9 = a, b9 = b as Element of SubstitutionSet (V,C) by SUBSTLAT:def_4;
 ( a9 in SubstitutionSet (V,C) & b9 in SubstitutionSet (V,C) ) ;
then reconsider a1 = a, b1 = b as Element of SubstitutionSet (V9,C9) by A5;
thus B1 . (a,b) = mi (a9 \/ b9) by SUBSTLAT:def_4
.= mi (a1 \/ b1) by A3, Th10
.= the L_join of (SubstLatt (V9,C9)) . (a,b) by SUBSTLAT:def_4
.= B2 . [a,b] by FUNCT_1:49
.= B2 . (a,b) ; ::_thesis: verum
end;
hence  the L_join of (SubstLatt (V,C)) = the L_join of (SubstLatt (V9,C9)) || the carrier of (SubstLatt (V,C)) by BINOP_1:2; ::_thesis: verum
end;

definition
let V, C be set ;
func SubstPoset (V,C) ->  RelStr  equals :: HEYTING3:def 1
 LattPOSet (SubstLatt (V,C));
coherence
 LattPOSet (SubstLatt (V,C)) is RelStr ;
end;

:: deftheorem  defines SubstPoset HEYTING3:def_1_:_
 for V, C being set holds SubstPoset (V,C) = LattPOSet (SubstLatt (V,C));

registration
let V, C be set ;
cluster SubstPoset (V,C) ->  with_suprema with_infima ;
coherence
 ( SubstPoset (V,C) is with_suprema & SubstPoset (V,C) is with_infima ) ;
end;

registration
let V, C be set ;
cluster SubstPoset (V,C) ->  reflexive transitive antisymmetric ;
coherence
 ( SubstPoset (V,C) is reflexive & SubstPoset (V,C) is antisymmetric & SubstPoset (V,C) is transitive ) ;
end;

theorem Th12: :: HEYTING3:12
for V, C being set
for a, b being Element of (SubstPoset (V,C)) holds
( a <= b iff for x being set st x in a holds
ex y being set st
( y in b & y c= x ) )
proof
let V, C be set ; ::_thesis: for a, b being Element of (SubstPoset (V,C)) holds
( a <= b iff for x being set st x in a holds
ex y being set st
( y in b & y c= x ) )
let a, b be Element of (SubstPoset (V,C)); ::_thesis: ( a <= b iff for x being set st x in a holds
ex y being set st
( y in b & y c= x ) )
reconsider a9 = a, b9 = b as Element of (SubstLatt (V,C)) ;
reconsider a1 = a, b1 = b as Element of SubstitutionSet (V,C) by SUBSTLAT:def_4;
A1: ( a9 % = a & b9 % = b ) ;
hereby  ::_thesis: ( ( for x being set st x in a holds
ex y being set st
( y in b & y c= x ) ) implies a <= b )
assume  a <= b ; ::_thesis: for x being set st x in a holds
ex y being set st
( y in b & y c= x )
then  a9 [= b9 by A1, LATTICE3:7;
then a9 = a9 "/\" b9 by LATTICES:4
.= the L_meet of (SubstLatt (V,C)) . (a9,b9) by LATTICES:def_2
.= mi (a1 ^ b1) by SUBSTLAT:def_4 ;
hence  for x being set st x in a holds
ex y being set st
( y in b & y c= x ) by HEYTING2:4; ::_thesis: verum
end;
assume  for x being set st x in a holds
ex y being set st
( y in b & y c= x ) ; ::_thesis: a <= b
then  mi (a1 ^ b1) = a1 by HEYTING2:5;
then a9 = the L_meet of (SubstLatt (V,C)) . (a9,b9) by SUBSTLAT:def_4
.= a9 "/\" b9 by LATTICES:def_2 ;
then  a9 [= b9 by LATTICES:4;
hence  a <= b by A1, LATTICE3:7; ::_thesis: verum
end;

theorem :: HEYTING3:13
for V, V9, C, C9 being set st V c= V9 & C c= C9 holds
SubstPoset (V,C) is full SubRelStr of SubstPoset (V9,C9)
proof
let V, V9, C, C9 be set ; ::_thesis: ( V c= V9 & C c= C9 implies SubstPoset (V,C) is full SubRelStr of SubstPoset (V9,C9) )
set K = SubstPoset (V,C);
set L = SubstPoset (V9,C9);
A1: ( the carrier of (SubstPoset (V,C)) = SubstitutionSet (V,C) & the carrier of (SubstPoset (V9,C9)) = SubstitutionSet (V9,C9) ) by SUBSTLAT:def_4;
assume  ( V c= V9 & C c= C9 ) ; ::_thesis: SubstPoset (V,C) is full SubRelStr of SubstPoset (V9,C9)
then A2: the carrier of (SubstPoset (V,C)) c= the carrier of (SubstPoset (V9,C9)) by A1, Th9;
now__::_thesis:_for_a,_b_being_set_st_[a,b]_in_the_InternalRel_of_(SubstPoset_(V,C))_holds_
[a,b]_in_the_InternalRel_of_(SubstPoset_(V9,C9))
let a, b be set ; ::_thesis: ( [a,b] in the InternalRel of (SubstPoset (V,C)) implies [a,b] in the InternalRel of (SubstPoset (V9,C9)) )
assume A3: [a,b] in the InternalRel of (SubstPoset (V,C)) ; ::_thesis: [a,b] in the InternalRel of (SubstPoset (V9,C9))
then reconsider a9 = a, b9 = b as Element of (SubstPoset (V,C)) by ZFMISC_1:87;
 ( a in the carrier of (SubstPoset (V,C)) & b in the carrier of (SubstPoset (V,C)) ) by A3, ZFMISC_1:87;
then reconsider a1 = a, b1 = b as Element of (SubstPoset (V9,C9)) by A2;
 a9 <= b9 by A3, ORDERS_2:def_5;
then  for x being set st x in a9 holds
ex y being set st
( y in b9 & y c= x ) by Th12;
then  a1 <= b1 by Th12;
hence  [a,b] in the InternalRel of (SubstPoset (V9,C9)) by ORDERS_2:def_5; ::_thesis: verum
end;
then  the InternalRel of (SubstPoset (V,C)) c= the InternalRel of (SubstPoset (V9,C9)) by RELAT_1:def_3;
then reconsider K = SubstPoset (V,C) as SubRelStr of SubstPoset (V9,C9) by A2, YELLOW_0:def_13;
now__::_thesis:_for_x,_y_being_set_st_[x,y]_in_the_InternalRel_of_(SubstPoset_(V9,C9))_|_2_the_carrier_of_K_holds_
[x,y]_in_the_InternalRel_of_K
let x, y be set ; ::_thesis: ( [x,y] in the InternalRel of (SubstPoset (V9,C9)) |_2 the carrier of K implies [x,y] in the InternalRel of K )
assume A4: [x,y] in the InternalRel of (SubstPoset (V9,C9)) |_2 the carrier of K ; ::_thesis: [x,y] in the InternalRel of K
then A5: [x,y] in the InternalRel of (SubstPoset (V9,C9)) by XBOOLE_0:def_4;
then reconsider p = x, q = y as Element of (SubstPoset (V9,C9)) by ZFMISC_1:87;
 [x,y] in [: the carrier of K, the carrier of K:] by A4, XBOOLE_0:def_4;
then reconsider p9 = x, q9 = y as Element of K by ZFMISC_1:87;
 p <= q by A5, ORDERS_2:def_5;
then  for a being set st a in p holds
ex b being set st
( b in q & b c= a ) by Th12;
then  p9 <= q9 by Th12;
hence  [x,y] in the InternalRel of K by ORDERS_2:def_5; ::_thesis: verum
end;
then A6: the InternalRel of (SubstPoset (V9,C9)) |_2 the carrier of K c= the InternalRel of K by RELAT_1:def_3;
now__::_thesis:_for_x,_y_being_set_st_[x,y]_in_the_InternalRel_of_K_holds_
[x,y]_in_the_InternalRel_of_(SubstPoset_(V9,C9))_|_2_the_carrier_of_K
let x, y be set ; ::_thesis: ( [x,y] in the InternalRel of K implies [x,y] in the InternalRel of (SubstPoset (V9,C9)) |_2 the carrier of K )
assume A7: [x,y] in the InternalRel of K ; ::_thesis: [x,y] in the InternalRel of (SubstPoset (V9,C9)) |_2 the carrier of K
then reconsider p = x, q = y as Element of K by ZFMISC_1:87;
 ( x in the carrier of K & y in the carrier of K ) by A7, ZFMISC_1:87;
then reconsider p9 = p, q9 = q as Element of (SubstPoset (V9,C9)) by A2;
 p <= q by A7, ORDERS_2:def_5;
then  for a being set st a in p holds
ex b being set st
( b in q & b c= a ) by Th12;
then  p9 <= q9 by Th12;
then  [p9,q9] in the InternalRel of (SubstPoset (V9,C9)) by ORDERS_2:def_5;
hence  [x,y] in the InternalRel of (SubstPoset (V9,C9)) |_2 the carrier of K by A7, XBOOLE_0:def_4; ::_thesis: verum
end;
then  the InternalRel of K c= the InternalRel of (SubstPoset (V9,C9)) |_2 the carrier of K by RELAT_1:def_3;
then  the InternalRel of K = the InternalRel of (SubstPoset (V9,C9)) |_2 the carrier of K by A6, XBOOLE_0:def_10;
hence  SubstPoset (V,C) is full SubRelStr of SubstPoset (V9,C9) by YELLOW_0:def_14; ::_thesis: verum
end;

definition
let n, k be Element of NAT ;
func PFArt (n,k) ->  Element of PFuncs (NAT,{k}) means :Def2: :: HEYTING3:def 2
 for x being set holds
( x in it iff ( ex m being odd Element of NAT st
( m <= 2 * n & [m,k] = x ) or [(2 * n),k] = x ) );
existence
 ex b1 being Element of PFuncs (NAT,{k}) st
for x being set holds
( x in b1 iff ( ex m being odd Element of NAT st
( m <= 2 * n & [m,k] = x ) or [(2 * n),k] = x ) )
proof
defpred S1[ set ] means ( ex m being odd Element of NAT st
( m <= 2 * n & [m,k] = $1 ) or [(2 * n),k] = $1 );
consider X being set  such that
A1: for x being set holds
( x in X iff ( x in [:NAT,{k}:] & S1[x] ) ) from XBOOLE_0:sch_1();
A2: X c= [:NAT,{k}:]
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in [:NAT,{k}:] )
assume  x in X ; ::_thesis: x in [:NAT,{k}:]
hence  x in [:NAT,{k}:] by A1; ::_thesis: verum
end;
then reconsider X9 = X as Function by GRFUNC_1:1;
 ( dom X9 c= NAT & rng X9 c= {k} ) by A2, SYSREL:3;
then reconsider X = X as Element of PFuncs (NAT,{k}) by PARTFUN1:def_3;
take  X ; ::_thesis: for x being set holds
( x in X iff ( ex m being odd Element of NAT st
( m <= 2 * n & [m,k] = x ) or [(2 * n),k] = x ) )
let x be set ; ::_thesis: ( x in X iff ( ex m being odd Element of NAT st
( m <= 2 * n & [m,k] = x ) or [(2 * n),k] = x ) )
thus  ( not x in X or ex m being odd Element of NAT st
( m <= 2 * n & [m,k] = x ) or [(2 * n),k] = x ) by A1; ::_thesis: ( ( ex m being odd Element of NAT st
( m <= 2 * n & [m,k] = x ) or [(2 * n),k] = x ) implies x in X )
assume A3: ( ex m being odd Element of NAT st
( m <= 2 * n & [m,k] = x ) or [(2 * n),k] = x ) ; ::_thesis: x in X
percases ( ex m being odd Element of NAT st
( m <= 2 * n & [m,k] = x ) or [(2 * n),k] = x ) by A3;
suppose ex m being odd Element of NAT st
( m <= 2 * n & [m,k] = x ) ; ::_thesis: x in X
then  x in [:NAT,{k}:] by ZFMISC_1:106;
hence  x in X by A1, A3; ::_thesis: verum
end;
supposeA4: [(2 * n),k] = x ; ::_thesis: x in X
then  x in [:NAT,{k}:] by ZFMISC_1:106;
hence  x in X by A1, A4; ::_thesis: verum
end;
end;
end;
uniqueness
 for b1, b2 being Element of PFuncs (NAT,{k}) st ( for x being set holds
( x in b1 iff ( ex m being odd Element of NAT st
( m <= 2 * n & [m,k] = x ) or [(2 * n),k] = x ) ) ) & ( for x being set holds
( x in b2 iff ( ex m being odd Element of NAT st
( m <= 2 * n & [m,k] = x ) or [(2 * n),k] = x ) ) ) holds
b1 = b2
proof
defpred S1[ set ] means ( ex m being odd Element of NAT st
( m <= 2 * n & [m,k] = $1 ) or [(2 * n),k] = $1 );
A5: for X1, X2 being Element of PFuncs (NAT,{k}) st ( for x being set holds
( x in X1 iff S1[x] ) ) & ( for x being set holds
( x in X2 iff S1[x] ) ) holds
X1 = X2 from LMOD_7:sch_1();
let X1, X2 be Element of PFuncs (NAT,{k}); ::_thesis: ( ( for x being set holds
( x in X1 iff ( ex m being odd Element of NAT st
( m <= 2 * n & [m,k] = x ) or [(2 * n),k] = x ) ) ) & ( for x being set holds
( x in X2 iff ( ex m being odd Element of NAT st
( m <= 2 * n & [m,k] = x ) or [(2 * n),k] = x ) ) ) implies X1 = X2 )
assume  ( ( for x being set holds
( x in X1 iff S1[x] ) ) & ( for x being set holds
( x in X2 iff S1[x] ) ) ) ; ::_thesis: X1 = X2
hence  X1 = X2 by A5; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines PFArt HEYTING3:def_2_:_
 for n, k being Element of NAT
for b3 being Element of PFuncs (NAT,{k}) holds
( b3 = PFArt (n,k) iff for x being set holds
( x in b3 iff ( ex m being odd Element of NAT st
( m <= 2 * n & [m,k] = x ) or [(2 * n),k] = x ) ) );

registration
let n, k be Element of NAT ;
cluster PFArt (n,k) ->  finite ;
coherence
 PFArt (n,k) is finite
proof
 PFArt (n,k) c= [:((Seg (2 * n)) \/ {0}),{k}:]
proof
let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in PFArt (n,k) or t in [:((Seg (2 * n)) \/ {0}),{k}:] )
assume A1: t in PFArt (n,k) ; ::_thesis: t in [:((Seg (2 * n)) \/ {0}),{k}:]
percases ( ex m1 being odd Element of NAT st
( m1 <= 2 * n & [m1,k] = t ) or [(2 * n),k] = t ) by A1, Def2;
suppose ex m1 being odd Element of NAT st
( m1 <= 2 * n & [m1,k] = t ) ; ::_thesis: t in [:((Seg (2 * n)) \/ {0}),{k}:]
then consider m1 being odd Element of NAT  such that
A2: m1 <= 2 * n and
A3: [m1,k] = t ;
 1 <= m1 by ABIAN:12;
then  m1 in Seg (2 * n) by A2, FINSEQ_1:1;
then  m1 in (Seg (2 * n)) \/ {0} by XBOOLE_0:def_3;
hence  t in [:((Seg (2 * n)) \/ {0}),{k}:] by A3, ZFMISC_1:106; ::_thesis: verum
end;
supposeA4: [(2 * n),k] = t ; ::_thesis: t in [:((Seg (2 * n)) \/ {0}),{k}:]
now__::_thesis:_t_in_[:((Seg_(2_*_n))_\/_{0}),{k}:]
percases ( not n is empty or n is empty ) ;
supposeA5: not n is empty ; ::_thesis: t in [:((Seg (2 * n)) \/ {0}),{k}:]
A6: n <= 2 * n by XREAL_1:151;
 1 <= n by A5, NAT_1:14;
then  1 <= 2 * n by A6, XXREAL_0:2;
then  2 * n in Seg (2 * n) by FINSEQ_1:1;
then  2 * n in (Seg (2 * n)) \/ {0} by XBOOLE_0:def_3;
hence  t in [:((Seg (2 * n)) \/ {0}),{k}:] by A4, ZFMISC_1:106; ::_thesis: verum
end;
suppose n is empty ; ::_thesis: t in [:((Seg (2 * n)) \/ {0}),{k}:]
then  2 * n in {0} by TARSKI:def_1;
then  2 * n in (Seg (2 * n)) \/ {0} by XBOOLE_0:def_3;
hence  t in [:((Seg (2 * n)) \/ {0}),{k}:] by A4, ZFMISC_1:106; ::_thesis: verum
end;
end;
end;
hence  t in [:((Seg (2 * n)) \/ {0}),{k}:] ; ::_thesis: verum
end;
end;
end;
hence  PFArt (n,k) is finite ; ::_thesis: verum
end;
end;

definition
let n, k be Element of NAT ;
func PFCrt (n,k) ->  Element of PFuncs (NAT,{k}) means :Def3: :: HEYTING3:def 3
 for x being set holds
( x in it iff ex m being odd Element of NAT st
( m <= (2 * n) + 1 & [m,k] = x ) );
existence
 ex b1 being Element of PFuncs (NAT,{k}) st
for x being set holds
( x in b1 iff ex m being odd Element of NAT st
( m <= (2 * n) + 1 & [m,k] = x ) )
proof
defpred S1[ set ] means  ex m being odd Element of NAT st
( m <= (2 * n) + 1 & [m,k] = $1 );
consider X being set  such that
A1: for x being set holds
( x in X iff ( x in [:NAT,{k}:] & S1[x] ) ) from XBOOLE_0:sch_1();
A2: X c= [:NAT,{k}:]
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in [:NAT,{k}:] )
assume  x in X ; ::_thesis: x in [:NAT,{k}:]
hence  x in [:NAT,{k}:] by A1; ::_thesis: verum
end;
then reconsider X9 = X as Function by GRFUNC_1:1;
 ( dom X9 c= NAT & rng X9 c= {k} ) by A2, SYSREL:3;
then reconsider X = X as Element of PFuncs (NAT,{k}) by PARTFUN1:def_3;
take  X ; ::_thesis: for x being set holds
( x in X iff ex m being odd Element of NAT st
( m <= (2 * n) + 1 & [m,k] = x ) )
let x be set ; ::_thesis: ( x in X iff ex m being odd Element of NAT st
( m <= (2 * n) + 1 & [m,k] = x ) )
thus  ( x in X implies ex m being odd Element of NAT st
( m <= (2 * n) + 1 & [m,k] = x ) ) by A1; ::_thesis: ( ex m being odd Element of NAT st
( m <= (2 * n) + 1 & [m,k] = x ) implies x in X )
given m being odd Element of NAT  such that A3: m <= (2 * n) + 1 and
A4: [m,k] = x ; ::_thesis: x in X
 x in [:NAT,{k}:] by A4, ZFMISC_1:106;
hence  x in X by A1, A3, A4; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Element of PFuncs (NAT,{k}) st ( for x being set holds
( x in b1 iff ex m being odd Element of NAT st
( m <= (2 * n) + 1 & [m,k] = x ) ) ) & ( for x being set holds
( x in b2 iff ex m being odd Element of NAT st
( m <= (2 * n) + 1 & [m,k] = x ) ) ) holds
b1 = b2
proof
defpred S1[ set ] means  ex m being odd Element of NAT st
( m <= (2 * n) + 1 & [m,k] = $1 );
A5: for X1, X2 being Element of PFuncs (NAT,{k}) st ( for x being set holds
( x in X1 iff S1[x] ) ) & ( for x being set holds
( x in X2 iff S1[x] ) ) holds
X1 = X2 from LMOD_7:sch_1();
let X1, X2 be Element of PFuncs (NAT,{k}); ::_thesis: ( ( for x being set holds
( x in X1 iff ex m being odd Element of NAT st
( m <= (2 * n) + 1 & [m,k] = x ) ) ) & ( for x being set holds
( x in X2 iff ex m being odd Element of NAT st
( m <= (2 * n) + 1 & [m,k] = x ) ) ) implies X1 = X2 )
assume  ( ( for x being set holds
( x in X1 iff S1[x] ) ) & ( for x being set holds
( x in X2 iff S1[x] ) ) ) ; ::_thesis: X1 = X2
hence  X1 = X2 by A5; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines PFCrt HEYTING3:def_3_:_
 for n, k being Element of NAT
for b3 being Element of PFuncs (NAT,{k}) holds
( b3 = PFCrt (n,k) iff for x being set holds
( x in b3 iff ex m being odd Element of NAT st
( m <= (2 * n) + 1 & [m,k] = x ) ) );

registration
let n, k be Element of NAT ;
cluster PFCrt (n,k) ->  finite ;
coherence
 PFCrt (n,k) is finite
proof
set x = PFCrt (n,k);
 PFCrt (n,k) c= [:(Seg ((2 * n) + 1)),{k}:]
proof
let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in PFCrt (n,k) or t in [:(Seg ((2 * n) + 1)),{k}:] )
assume  t in PFCrt (n,k) ; ::_thesis: t in [:(Seg ((2 * n) + 1)),{k}:]
then consider m being odd Element of NAT  such that
A1: m <= (2 * n) + 1 and
A2: [m,k] = t by Def3;
 1 <= m by ABIAN:12;
then  m in Seg ((2 * n) + 1) by A1, FINSEQ_1:1;
hence  t in [:(Seg ((2 * n) + 1)),{k}:] by A2, ZFMISC_1:106; ::_thesis: verum
end;
hence  PFCrt (n,k) is finite ; ::_thesis: verum
end;
end;

theorem :: HEYTING3:14
for n, k being Element of NAT holds [((2 * n) + 1),k] in PFCrt (n,k) by Def3;

theorem Th15: :: HEYTING3:15
for n, k being Element of NAT holds PFCrt (n,k) misses {[((2 * n) + 3),k]}
proof
let n, k be Element of NAT ; ::_thesis: PFCrt (n,k) misses {[((2 * n) + 3),k]}
assume  (PFCrt (n,k)) /\ {[((2 * n) + 3),k]} <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction
then consider x being set  such that
A1: x in (PFCrt (n,k)) /\ {[((2 * n) + 3),k]} by XBOOLE_0:def_1;
 x in PFCrt (n,k) by A1, XBOOLE_0:def_4;
then consider m being odd Element of NAT  such that
A2: m <= (2 * n) + 1 and
A3: [m,k] = x by Def3;
 x in {[((2 * n) + 3),k]} by A1, XBOOLE_0:def_4;
then  x = [((2 * n) + 3),k] by TARSKI:def_1;
then  m = (2 * n) + 3 by A3, XTUPLE_0:1;
hence  contradiction by A2, XREAL_1:6; ::_thesis: verum
end;

Lm4:  for n being Element of NAT holds (2 * n) + 1 <= (2 * (n + 1)) + 1
proof
let n be Element of NAT ; ::_thesis: (2 * n) + 1 <= (2 * (n + 1)) + 1
 (2 * (n + 1)) + 1 = ((2 * n) + 1) + 2 ;
hence  (2 * n) + 1 <= (2 * (n + 1)) + 1 by NAT_1:11; ::_thesis: verum
end;

theorem Th16: :: HEYTING3:16
for n, k being Element of NAT holds PFCrt ((n + 1),k) = (PFCrt (n,k)) \/ {[((2 * n) + 3),k]}
proof
let n, k be Element of NAT ; ::_thesis: PFCrt ((n + 1),k) = (PFCrt (n,k)) \/ {[((2 * n) + 3),k]}
A1: (2 * (n + 1)) + 1 = (2 * n) + 3 ;
thus  PFCrt ((n + 1),k) c= (PFCrt (n,k)) \/ {[((2 * n) + 3),k]} :: according to XBOOLE_0:def_10 ::_thesis: (PFCrt (n,k)) \/ {[((2 * n) + 3),k]} c= PFCrt ((n + 1),k)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in PFCrt ((n + 1),k) or x in (PFCrt (n,k)) \/ {[((2 * n) + 3),k]} )
assume  x in PFCrt ((n + 1),k) ; ::_thesis: x in (PFCrt (n,k)) \/ {[((2 * n) + 3),k]}
then consider m being odd Element of NAT  such that
A2: m <= (2 * (n + 1)) + 1 and
A3: [m,k] = x by Def3;
percases ( m <= 2 * (n + 1) or m = (2 * (n + 1)) + 1 ) by A2, NAT_1:9;
suppose m <= 2 * (n + 1) ; ::_thesis: x in (PFCrt (n,k)) \/ {[((2 * n) + 3),k]}
then  ( m <= (2 * n) + 1 or m = ((2 * n) + 1) + 1 ) by NAT_1:8;
then  x in PFCrt (n,k) by A3, Def3;
hence  x in (PFCrt (n,k)) \/ {[((2 * n) + 3),k]} by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose m = (2 * (n + 1)) + 1 ; ::_thesis: x in (PFCrt (n,k)) \/ {[((2 * n) + 3),k]}
then  x in {[((2 * n) + 3),k]} by A3, TARSKI:def_1;
hence  x in (PFCrt (n,k)) \/ {[((2 * n) + 3),k]} by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (PFCrt (n,k)) \/ {[((2 * n) + 3),k]} or x in PFCrt ((n + 1),k) )
assume A4: x in (PFCrt (n,k)) \/ {[((2 * n) + 3),k]} ; ::_thesis: x in PFCrt ((n + 1),k)
percases ( x in PFCrt (n,k) or x in {[((2 * n) + 3),k]} ) by A4, XBOOLE_0:def_3;
suppose x in PFCrt (n,k) ; ::_thesis: x in PFCrt ((n + 1),k)
then consider m being odd Element of NAT  such that
A5: m <= (2 * n) + 1 and
A6: [m,k] = x by Def3;
 (2 * n) + 1 <= (2 * (n + 1)) + 1 by Lm4;
then  m <= (2 * (n + 1)) + 1 by A5, XXREAL_0:2;
hence  x in PFCrt ((n + 1),k) by A6, Def3; ::_thesis: verum
end;
suppose x in {[((2 * n) + 3),k]} ; ::_thesis: x in PFCrt ((n + 1),k)
then  x = [((2 * n) + 3),k] by TARSKI:def_1;
hence  x in PFCrt ((n + 1),k) by A1, Def3; ::_thesis: verum
end;
end;
end;

Lm5:  for n, n9 being Element of NAT holds not PFCrt ((n + 1),n9) c= PFCrt (n,n9)
proof
let n, n9 be Element of NAT ; ::_thesis: not PFCrt ((n + 1),n9) c= PFCrt (n,n9)
set k = [((2 * n) + 3),n9];
 PFCrt ((n + 1),n9) = (PFCrt (n,n9)) \/ {[((2 * n) + 3),n9]} by Th16;
then  {[((2 * n) + 3),n9]} c= PFCrt ((n + 1),n9) by XBOOLE_1:7;
then A1: [((2 * n) + 3),n9] in PFCrt ((n + 1),n9) by ZFMISC_1:31;
 PFCrt (n,n9) misses {[((2 * n) + 3),n9]} by Th15;
then  (PFCrt (n,n9)) /\ {[((2 * n) + 3),n9]} = {} by XBOOLE_0:def_7;
hence  not PFCrt ((n + 1),n9) c= PFCrt (n,n9) by A1, ZFMISC_1:46; ::_thesis: verum
end;

theorem Th17: :: HEYTING3:17
for n, k being Element of NAT holds PFCrt (n,k) c< PFCrt ((n + 1),k)
proof
let n, k be Element of NAT ; ::_thesis: PFCrt (n,k) c< PFCrt ((n + 1),k)
thus  PFCrt (n,k) c= PFCrt ((n + 1),k) :: according to XBOOLE_0:def_8 ::_thesis: not PFCrt (n,k) = PFCrt ((n + 1),k)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in PFCrt (n,k) or x in PFCrt ((n + 1),k) )
assume  x in PFCrt (n,k) ; ::_thesis: x in PFCrt ((n + 1),k)
then consider m being odd Element of NAT  such that
A1: m <= (2 * n) + 1 and
A2: [m,k] = x by Def3;
 (2 * n) + 1 <= (2 * (n + 1)) + 1 by Lm4;
then  m <= (2 * (n + 1)) + 1 by A1, XXREAL_0:2;
hence  x in PFCrt ((n + 1),k) by A2, Def3; ::_thesis: verum
end;
thus  not PFCrt (n,k) = PFCrt ((n + 1),k) by Lm5; ::_thesis: verum
end;

registration
let n, k be Element of NAT ;
cluster PFArt (n,k) ->  non empty ;
coherence
 not PFArt (n,k) is empty
proof
 [(2 * n),k] in PFArt (n,k) by Def2;
hence  not PFArt (n,k) is empty ; ::_thesis: verum
end;
end;

theorem Th18: :: HEYTING3:18
for n, m, k being Element of NAT holds not PFArt (n,m) c= PFCrt (k,m)
proof
let n, m, k be Element of NAT ; ::_thesis: not PFArt (n,m) c= PFCrt (k,m)
set x = [(2 * n),m];
A1: not [(2 * n),m] in PFCrt (k,m)
proof
assume  [(2 * n),m] in PFCrt (k,m) ; ::_thesis: contradiction
then  ex m9 being odd Element of NAT st
( m9 <= (2 * k) + 1 & [m9,m] = [(2 * n),m] ) by Def3;
hence  contradiction by XTUPLE_0:1; ::_thesis: verum
end;
 [(2 * n),m] in PFArt (n,m) by Def2;
hence  not PFArt (n,m) c= PFCrt (k,m) by A1; ::_thesis: verum
end;

Lm6:  for n, k being Element of NAT holds PFCrt (n,k) c= PFCrt ((n + 1),k)
proof
let n, k be Element of NAT ; ::_thesis: PFCrt (n,k) c= PFCrt ((n + 1),k)
 PFCrt (n,k) c< PFCrt ((n + 1),k) by Th17;
hence  PFCrt (n,k) c= PFCrt ((n + 1),k) by XBOOLE_0:def_8; ::_thesis: verum
end;

theorem :: HEYTING3:19
for n, m, k being Element of NAT st n <= k holds
PFCrt (n,m) c= PFCrt (k,m)
proof
let n, m, k be Element of NAT ; ::_thesis: ( n <= k implies PFCrt (n,m) c= PFCrt (k,m) )
assume  n <= k ; ::_thesis: PFCrt (n,m) c= PFCrt (k,m)
then  2 * n <= 2 * k by NAT_1:4;
then A1: (2 * n) + 1 <= (2 * k) + 1 by XREAL_1:6;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in PFCrt (n,m) or x in PFCrt (k,m) )
assume  x in PFCrt (n,m) ; ::_thesis: x in PFCrt (k,m)
then consider m9 being odd Element of NAT  such that
A2: m9 <= (2 * n) + 1 and
A3: [m9,m] = x by Def3;
 m9 <= (2 * k) + 1 by A1, A2, XXREAL_0:2;
hence  x in PFCrt (k,m) by A3, Def3; ::_thesis: verum
end;

Lm7:  for n, m, k being Element of NAT st n < k holds
PFCrt (n,m) c= PFArt (k,m)
proof
let n, m, k be Element of NAT ; ::_thesis: ( n < k implies PFCrt (n,m) c= PFArt (k,m) )
assume  n < k ; ::_thesis: PFCrt (n,m) c= PFArt (k,m)
then  2 * n < 2 * k by XREAL_1:68;
then A1: (2 * n) + 1 <= 2 * k by NAT_1:13;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in PFCrt (n,m) or x in PFArt (k,m) )
assume  x in PFCrt (n,m) ; ::_thesis: x in PFArt (k,m)
then consider p being odd Element of NAT  such that
A2: p <= (2 * n) + 1 and
A3: [p,m] = x by Def3;
 p <= 2 * k by A1, A2, XXREAL_0:2;
hence  x in PFArt (k,m) by A3, Def2; ::_thesis: verum
end;

theorem :: HEYTING3:20
for n being Element of NAT holds PFArt (1,n) = {[1,n],[2,n]}
proof
let n be Element of NAT ; ::_thesis: PFArt (1,n) = {[1,n],[2,n]}
thus  PFArt (1,n) c= {[1,n],[2,n]} :: according to XBOOLE_0:def_10 ::_thesis: {[1,n],[2,n]} c= PFArt (1,n)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in PFArt (1,n) or x in {[1,n],[2,n]} )
assume A1: x in PFArt (1,n) ; ::_thesis: x in {[1,n],[2,n]}
percases ( ex m being odd Element of NAT st
( m <= 2 * 1 & [m,n] = x ) or [(2 * 1),n] = x ) by A1, Def2;
suppose ex m being odd Element of NAT st
( m <= 2 * 1 & [m,n] = x ) ; ::_thesis: x in {[1,n],[2,n]}
then  x = [1,n] by NAT_1:26;
hence  x in {[1,n],[2,n]} by TARSKI:def_2; ::_thesis: verum
end;
suppose [(2 * 1),n] = x ; ::_thesis: x in {[1,n],[2,n]}
hence  x in {[1,n],[2,n]} by TARSKI:def_2; ::_thesis: verum
end;
end;
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {[1,n],[2,n]} or x in PFArt (1,n) )
assume A2: x in {[1,n],[2,n]} ; ::_thesis: x in PFArt (1,n)
percases ( x = [1,n] or x = [2,n] ) by A2, TARSKI:def_2;
supposeA3: x = [1,n] ; ::_thesis: x in PFArt (1,n)
 1 <= 2 * 1 ;
hence  x in PFArt (1,n) by A3, Def2, Lm2, Lm3; ::_thesis: verum
end;
suppose x = [2,n] ; ::_thesis: x in PFArt (1,n)
then  x = [(2 * 1),n] ;
hence  x in PFArt (1,n) by Def2; ::_thesis: verum
end;
end;
end;

definition
let n, k be Element of NAT ;
func PFBrt (n,k) ->  Element of Fin (PFuncs (NAT,{k})) means :Def4: :: HEYTING3:def 4
 for x being set holds
( x in it iff ( ex m being non empty Element of NAT st
( m <= n & x = PFArt (m,k) ) or x = PFCrt (n,k) ) );
existence
 ex b1 being Element of Fin (PFuncs (NAT,{k})) st
for x being set holds
( x in b1 iff ( ex m being non empty Element of NAT st
( m <= n & x = PFArt (m,k) ) or x = PFCrt (n,k) ) )
proof
defpred S1[ set ] means ( ex m being non empty Element of NAT st
( m <= n & $1 = PFArt (m,k) ) or $1 = PFCrt (n,k) );
consider X being set  such that
A1: for x being set holds
( x in X iff ( x in PFuncs (NAT,{k}) & S1[x] ) ) from XBOOLE_0:sch_1();
A2: X c= bool [:(Seg ((2 * n) + 1)),{k}:]
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in bool [:(Seg ((2 * n) + 1)),{k}:] )
assume A3: x in X ; ::_thesis: x in bool [:(Seg ((2 * n) + 1)),{k}:]
percases ( ex m being non empty Element of NAT st
( m <= n & x = PFArt (m,k) ) or x = PFCrt (n,k) ) by A1, A3;
supposeA4: ex m being non empty Element of NAT st
( m <= n & x = PFArt (m,k) ) ; ::_thesis: x in bool [:(Seg ((2 * n) + 1)),{k}:]
A5: 2 * n <= (2 * n) + 1 by NAT_1:11;
consider m being non empty Element of NAT  such that
A6: m <= n and
A7: x = PFArt (m,k) by A4;
 2 * m <= 2 * n by A6, NAT_1:4;
then A8: 2 * m <= (2 * n) + 1 by A5, XXREAL_0:2;
 x c= [:(Seg ((2 * n) + 1)),{k}:]
proof
let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in x or t in [:(Seg ((2 * n) + 1)),{k}:] )
assume A9: t in x ; ::_thesis: t in [:(Seg ((2 * n) + 1)),{k}:]
percases ( ex m1 being odd Element of NAT st
( m1 <= 2 * m & [m1,k] = t ) or [(2 * m),k] = t ) by A7, A9, Def2;
suppose ex m1 being odd Element of NAT st
( m1 <= 2 * m & [m1,k] = t ) ; ::_thesis: t in [:(Seg ((2 * n) + 1)),{k}:]
then consider m1 being odd Element of NAT  such that
A10: m1 <= 2 * m and
A11: [m1,k] = t ;
A12: 1 <= m1 by ABIAN:12;
 m1 <= (2 * n) + 1 by A8, A10, XXREAL_0:2;
then  m1 in Seg ((2 * n) + 1) by A12, FINSEQ_1:1;
hence  t in [:(Seg ((2 * n) + 1)),{k}:] by A11, ZFMISC_1:106; ::_thesis: verum
end;
supposeA13: [(2 * m),k] = t ; ::_thesis: t in [:(Seg ((2 * n) + 1)),{k}:]
 m <= 2 * m by XREAL_1:151;
then  1 <= 2 * m by NAT_1:14;
then  2 * m in Seg ((2 * n) + 1) by A8, FINSEQ_1:1;
hence  t in [:(Seg ((2 * n) + 1)),{k}:] by A13, ZFMISC_1:106; ::_thesis: verum
end;
end;
end;
hence  x in bool [:(Seg ((2 * n) + 1)),{k}:] ; ::_thesis: verum
end;
supposeA14: x = PFCrt (n,k) ; ::_thesis: x in bool [:(Seg ((2 * n) + 1)),{k}:]
 x c= [:(Seg ((2 * n) + 1)),{k}:]
proof
let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in x or t in [:(Seg ((2 * n) + 1)),{k}:] )
assume  t in x ; ::_thesis: t in [:(Seg ((2 * n) + 1)),{k}:]
then consider m being odd Element of NAT  such that
A15: m <= (2 * n) + 1 and
A16: [m,k] = t by A14, Def3;
 1 <= m by ABIAN:12;
then  m in Seg ((2 * n) + 1) by A15, FINSEQ_1:1;
hence  t in [:(Seg ((2 * n) + 1)),{k}:] by A16, ZFMISC_1:106; ::_thesis: verum
end;
hence  x in bool [:(Seg ((2 * n) + 1)),{k}:] ; ::_thesis: verum
end;
end;
end;
 X c= PFuncs (NAT,{k})
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in PFuncs (NAT,{k}) )
assume  x in X ; ::_thesis: x in PFuncs (NAT,{k})
hence  x in PFuncs (NAT,{k}) by A1; ::_thesis: verum
end;
then reconsider X = X as Element of Fin (PFuncs (NAT,{k})) by A2, FINSUB_1:def_5;
take  X ; ::_thesis: for x being set holds
( x in X iff ( ex m being non empty Element of NAT st
( m <= n & x = PFArt (m,k) ) or x = PFCrt (n,k) ) )
let x be set ; ::_thesis: ( x in X iff ( ex m being non empty Element of NAT st
( m <= n & x = PFArt (m,k) ) or x = PFCrt (n,k) ) )
thus  ( not x in X or ex m being non empty Element of NAT st
( m <= n & x = PFArt (m,k) ) or x = PFCrt (n,k) ) by A1; ::_thesis: ( ( ex m being non empty Element of NAT st
( m <= n & x = PFArt (m,k) ) or x = PFCrt (n,k) ) implies x in X )
assume  ( ex m being non empty Element of NAT st
( m <= n & x = PFArt (m,k) ) or x = PFCrt (n,k) ) ; ::_thesis: x in X
hence  x in X by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Element of Fin (PFuncs (NAT,{k})) st ( for x being set holds
( x in b1 iff ( ex m being non empty Element of NAT st
( m <= n & x = PFArt (m,k) ) or x = PFCrt (n,k) ) ) ) & ( for x being set holds
( x in b2 iff ( ex m being non empty Element of NAT st
( m <= n & x = PFArt (m,k) ) or x = PFCrt (n,k) ) ) ) holds
b1 = b2
proof
defpred S1[ set ] means ( ex m being non empty Element of NAT st
( m <= n & $1 = PFArt (m,k) ) or $1 = PFCrt (n,k) );
A17: for X1, X2 being Element of Fin (PFuncs (NAT,{k})) st ( for x being set holds
( x in X1 iff S1[x] ) ) & ( for x being set holds
( x in X2 iff S1[x] ) ) holds
X1 = X2 from LMOD_7:sch_1();
let X1, X2 be Element of Fin (PFuncs (NAT,{k})); ::_thesis: ( ( for x being set holds
( x in X1 iff ( ex m being non empty Element of NAT st
( m <= n & x = PFArt (m,k) ) or x = PFCrt (n,k) ) ) ) & ( for x being set holds
( x in X2 iff ( ex m being non empty Element of NAT st
( m <= n & x = PFArt (m,k) ) or x = PFCrt (n,k) ) ) ) implies X1 = X2 )
assume  ( ( for x being set holds
( x in X1 iff S1[x] ) ) & ( for x being set holds
( x in X2 iff S1[x] ) ) ) ; ::_thesis: X1 = X2
hence  X1 = X2 by A17; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines PFBrt HEYTING3:def_4_:_
 for n, k being Element of NAT
for b3 being Element of Fin (PFuncs (NAT,{k})) holds
( b3 = PFBrt (n,k) iff for x being set holds
( x in b3 iff ( ex m being non empty Element of NAT st
( m <= n & x = PFArt (m,k) ) or x = PFCrt (n,k) ) ) );

theorem :: HEYTING3:21
for n, k being Element of NAT
for x being set st x in PFBrt ((n + 1),k) holds
ex y being set st
( y in PFBrt (n,k) & y c= x )
proof
let n, k be Element of NAT ; ::_thesis: for x being set st x in PFBrt ((n + 1),k) holds
ex y being set st
( y in PFBrt (n,k) & y c= x )
let x be set ; ::_thesis: ( x in PFBrt ((n + 1),k) implies ex y being set st
( y in PFBrt (n,k) & y c= x ) )
assume A1: x in PFBrt ((n + 1),k) ; ::_thesis: ex y being set st
( y in PFBrt (n,k) & y c= x )
percases ( ex m being non empty Element of NAT st
( m <= n + 1 & x = PFArt (m,k) ) or x = PFCrt ((n + 1),k) ) by A1, Def4;
suppose ex m being non empty Element of NAT st
( m <= n + 1 & x = PFArt (m,k) ) ; ::_thesis: ex y being set st
( y in PFBrt (n,k) & y c= x )
then consider m being non empty Element of NAT  such that
A2: m <= n + 1 and
A3: x = PFArt (m,k) ;
thus  ex y being set st
( y in PFBrt (n,k) & y c= x ) ::_thesis: verum
proof
percases ( m <= n or m = n + 1 ) by A2, NAT_1:8;
supposeA4: m <= n ; ::_thesis: ex y being set st
( y in PFBrt (n,k) & y c= x )
take y = x; ::_thesis: ( y in PFBrt (n,k) & y c= x )
thus  y in PFBrt (n,k) by A3, A4, Def4; ::_thesis: y c= x
thus  y c= x ; ::_thesis: verum
end;
supposeA5: m = n + 1 ; ::_thesis: ex y being set st
( y in PFBrt (n,k) & y c= x )
take  PFCrt (n,k) ; ::_thesis: ( PFCrt (n,k) in PFBrt (n,k) & PFCrt (n,k) c= x )
 n < n + 1 by NAT_1:13;
hence  ( PFCrt (n,k) in PFBrt (n,k) & PFCrt (n,k) c= x ) by A3, A5, Def4, Lm7; ::_thesis: verum
end;
end;
end;
end;
supposeA6: x = PFCrt ((n + 1),k) ; ::_thesis: ex y being set st
( y in PFBrt (n,k) & y c= x )
take y = PFCrt (n,k); ::_thesis: ( y in PFBrt (n,k) & y c= x )
thus  y in PFBrt (n,k) by Def4; ::_thesis: y c= x
thus  y c= x by A6, Lm6; ::_thesis: verum
end;
end;
end;

theorem :: HEYTING3:22
for n, k being Element of NAT holds not PFCrt (n,k) in PFBrt ((n + 1),k)
proof
let n, k be Element of NAT ; ::_thesis: not PFCrt (n,k) in PFBrt ((n + 1),k)
assume  PFCrt (n,k) in PFBrt ((n + 1),k) ; ::_thesis: contradiction
then  ( ex m being non empty Element of NAT st
( m <= n + 1 & PFCrt (n,k) = PFArt (m,k) ) or PFCrt (n,k) = PFCrt ((n + 1),k) ) by Def4;
hence  contradiction by Th17, Th18; ::_thesis: verum
end;

Lm8:  for n, k being Element of NAT
for x being set st x in PFBrt (n,k) holds
x is finite
proof
let n, k be Element of NAT ; ::_thesis: for x being set st x in PFBrt (n,k) holds
x is finite
let x be set ; ::_thesis: ( x in PFBrt (n,k) implies x is finite )
assume  x in PFBrt (n,k) ; ::_thesis: x is finite
then A1: ( ex m being non empty Element of NAT st
( m <= n & x = PFArt (m,k) ) or x = PFCrt (n,k) ) by Def4;
percases ( ex m being Element of NAT st
( m <= n & x = PFArt (m,k) ) or x = PFCrt (n,k) ) by A1;
suppose ex m being Element of NAT st
( m <= n & x = PFArt (m,k) ) ; ::_thesis: x is finite
hence  x is finite ; ::_thesis: verum
end;
suppose x = PFCrt (n,k) ; ::_thesis: x is finite
hence  x is finite ; ::_thesis: verum
end;
end;
end;

theorem Th23: :: HEYTING3:23
for n, m, k being Element of NAT st PFArt (n,m) c= PFArt (k,m) holds
n = k
proof
let n, m, k be Element of NAT ; ::_thesis: ( PFArt (n,m) c= PFArt (k,m) implies n = k )
assume A1: PFArt (n,m) c= PFArt (k,m) ; ::_thesis: n = k
assume  n <> k ; ::_thesis: contradiction
then  2 * n <> 2 * k ;
then A2: [(2 * n),m] <> [(2 * k),m] by XTUPLE_0:1;
 [(2 * n),m] in PFArt (n,m) by Def2;
then  ex m9 being odd Element of NAT st
( m9 <= 2 * k & [m9,m] = [(2 * n),m] ) by A1, A2, Def2;
hence  contradiction by XTUPLE_0:1; ::_thesis: verum
end;

theorem Th24: :: HEYTING3:24
for n, m, k being Element of NAT holds
( PFCrt (n,m) c= PFArt (k,m) iff n < k )
proof
let n, m, k be Element of NAT ; ::_thesis: ( PFCrt (n,m) c= PFArt (k,m) iff n < k )
thus  ( PFCrt (n,m) c= PFArt (k,m) implies n < k ) ::_thesis: ( n < k implies PFCrt (n,m) c= PFArt (k,m) )
proof
assume A1: PFCrt (n,m) c= PFArt (k,m) ; ::_thesis: n < k
assume A2: k <= n ; ::_thesis: contradiction
A3: not [((2 * n) + 1),m] in PFArt (k,m)
proof
assume A4: [((2 * n) + 1),m] in PFArt (k,m) ; ::_thesis: contradiction
percases ( ex m9 being odd Element of NAT st
( m9 <= 2 * k & [m9,m] = [((2 * n) + 1),m] ) or [(2 * k),m] = [((2 * n) + 1),m] ) by A4, Def2;
supposeA5: ex m9 being odd Element of NAT st
( m9 <= 2 * k & [m9,m] = [((2 * n) + 1),m] ) ; ::_thesis: contradiction
A6: 2 * k <= 2 * n by A2, NAT_1:4;
 (2 * n) + 1 <= 2 * k by A5, XTUPLE_0:1;
hence  contradiction by A6, NAT_1:13; ::_thesis: verum
end;
suppose [(2 * k),m] = [((2 * n) + 1),m] ; ::_thesis: contradiction
hence  contradiction by XTUPLE_0:1; ::_thesis: verum
end;
end;
end;
 [((2 * n) + 1),m] in PFCrt (n,m) by Def3;
hence  contradiction by A1, A3; ::_thesis: verum
end;
thus  ( n < k implies PFCrt (n,m) c= PFArt (k,m) ) by Lm7; ::_thesis: verum
end;

begin

theorem Th25: :: HEYTING3:25
for n, k being Element of NAT holds PFBrt (n,k) is Element of (SubstPoset (NAT,{k}))
proof
let n, k be Element of NAT ; ::_thesis: PFBrt (n,k) is Element of (SubstPoset (NAT,{k}))
A1: for s, t being Element of PFuncs (NAT,{k}) st s in PFBrt (n,k) & t in PFBrt (n,k) & s c= t holds
s = t
proof
let s, t be Element of PFuncs (NAT,{k}); ::_thesis: ( s in PFBrt (n,k) & t in PFBrt (n,k) & s c= t implies s = t )
assume that
A2: s in PFBrt (n,k) and
A3: t in PFBrt (n,k) and
A4: s c= t ; ::_thesis: s = t
A5: ( ex m being non empty Element of NAT st
( m <= n & s = PFArt (m,k) ) or s = PFCrt (n,k) ) by A2, Def4;
A6: ( ex m being non empty Element of NAT st
( m <= n & t = PFArt (m,k) ) or t = PFCrt (n,k) ) by A3, Def4;
percases ( ( ex m being Element of NAT st
( m <= n & s = PFArt (m,k) ) & ex m being Element of NAT st
( m <= n & t = PFArt (m,k) ) ) or ( ex m being Element of NAT st
( m <= n & s = PFArt (m,k) ) & t = PFCrt (n,k) ) or ( s = PFCrt (n,k) & ex m being Element of NAT st
( m <= n & t = PFArt (m,k) ) ) or ( s = PFCrt (n,k) & t = PFCrt (n,k) ) ) by A5, A6;
suppose ( ex m being Element of NAT st
( m <= n & s = PFArt (m,k) ) & ex m being Element of NAT st
( m <= n & t = PFArt (m,k) ) ) ; ::_thesis: s = t
hence  s = t by A4, Th23; ::_thesis: verum
end;
suppose ( ex m being Element of NAT st
( m <= n & s = PFArt (m,k) ) & t = PFCrt (n,k) ) ; ::_thesis: s = t
hence  s = t by A4, Th18; ::_thesis: verum
end;
suppose ( s = PFCrt (n,k) & ex m being Element of NAT st
( m <= n & t = PFArt (m,k) ) ) ; ::_thesis: s = t
hence  s = t by A4, Th24; ::_thesis: verum
end;
suppose ( s = PFCrt (n,k) & t = PFCrt (n,k) ) ; ::_thesis: s = t
hence  s = t ; ::_thesis: verum
end;
end;
end;
 for u being set st u in PFBrt (n,k) holds
u is finite by Lm8;
then  ( SubstitutionSet (NAT,{k}) = the carrier of (SubstPoset (NAT,{k})) & PFBrt (n,k) in  {  A where A is Element of Fin (PFuncs (NAT,{k})) : ( ( for u being set st u in A holds
u is finite ) & ( for s, t being Element of PFuncs (NAT,{k}) st s in A & t in A & s c= t holds
s = t ) )  }  ) by A1, SUBSTLAT:def_4;
hence  PFBrt (n,k) is Element of (SubstPoset (NAT,{k})) by SUBSTLAT:def_1; ::_thesis: verum
end;

definition
let k be Element of NAT ;
func PFDrt k ->  Subset of (SubstPoset (NAT,{k})) means :Def5: :: HEYTING3:def 5
 for x being set holds
( x in it iff ex n being non empty Element of NAT st x = PFBrt (n,k) );
existence
 ex b1 being Subset of (SubstPoset (NAT,{k})) st
for x being set holds
( x in b1 iff ex n being non empty Element of NAT st x = PFBrt (n,k) )
proof
defpred S1[ set ] means  ex n being non empty Element of NAT st $1 = PFBrt (n,k);
consider X being set  such that
A1: for x being set holds
( x in X iff ( x in the carrier of (SubstPoset (NAT,{k})) & S1[x] ) ) from XBOOLE_0:sch_1();
 X c= the carrier of (SubstPoset (NAT,{k}))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in the carrier of (SubstPoset (NAT,{k})) )
assume  x in X ; ::_thesis: x in the carrier of (SubstPoset (NAT,{k}))
hence  x in the carrier of (SubstPoset (NAT,{k})) by A1; ::_thesis: verum
end;
then reconsider X9 = X as Subset of (SubstPoset (NAT,{k})) ;
take  X9 ; ::_thesis: for x being set holds
( x in X9 iff ex n being non empty Element of NAT st x = PFBrt (n,k) )
let x be set ; ::_thesis: ( x in X9 iff ex n being non empty Element of NAT st x = PFBrt (n,k) )
thus  ( x in X9 implies ex n being non empty Element of NAT st x = PFBrt (n,k) ) by A1; ::_thesis: ( ex n being non empty Element of NAT st x = PFBrt (n,k) implies x in X9 )
given n being non empty Element of NAT  such that A2: x = PFBrt (n,k) ; ::_thesis: x in X9
 x is Element of (SubstPoset (NAT,{k})) by A2, Th25;
hence  x in X9 by A1, A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset of (SubstPoset (NAT,{k})) st ( for x being set holds
( x in b1 iff ex n being non empty Element of NAT st x = PFBrt (n,k) ) ) & ( for x being set holds
( x in b2 iff ex n being non empty Element of NAT st x = PFBrt (n,k) ) ) holds
b1 = b2
proof
defpred S1[ set ] means  ex n being non empty Element of NAT st $1 = PFBrt (n,k);
A3: for A1, A2 being Subset of (SubstPoset (NAT,{k})) st ( for x being set holds
( x in A1 iff S1[x] ) ) & ( for x being set holds
( x in A2 iff S1[x] ) ) holds
A1 = A2 from HEYTING3:sch_1();
let A1, A2 be Subset of (SubstPoset (NAT,{k})); ::_thesis: ( ( for x being set holds
( x in A1 iff ex n being non empty Element of NAT st x = PFBrt (n,k) ) ) & ( for x being set holds
( x in A2 iff ex n being non empty Element of NAT st x = PFBrt (n,k) ) ) implies A1 = A2 )
assume  ( ( for x being set holds
( x in A1 iff S1[x] ) ) & ( for x being set holds
( x in A2 iff S1[x] ) ) ) ; ::_thesis: A1 = A2
hence  A1 = A2 by A3; ::_thesis: verum
end;
end;

:: deftheorem Def5 defines PFDrt HEYTING3:def_5_:_
 for k being Element of NAT
for b2 being Subset of (SubstPoset (NAT,{k})) holds
( b2 = PFDrt k iff for x being set holds
( x in b2 iff ex n being non empty Element of NAT st x = PFBrt (n,k) ) );

theorem :: HEYTING3:26
for k being Element of NAT holds PFBrt (1,k) = {(PFArt (1,k)),(PFCrt (1,k))}
proof
let k be Element of NAT ; ::_thesis: PFBrt (1,k) = {(PFArt (1,k)),(PFCrt (1,k))}
thus  PFBrt (1,k) c= {(PFArt (1,k)),(PFCrt (1,k))} :: according to XBOOLE_0:def_10 ::_thesis: {(PFArt (1,k)),(PFCrt (1,k))} c= PFBrt (1,k)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in PFBrt (1,k) or x in {(PFArt (1,k)),(PFCrt (1,k))} )
assume A1: x in PFBrt (1,k) ; ::_thesis: x in {(PFArt (1,k)),(PFCrt (1,k))}
percases ( ex m being non empty Element of NAT st
( m <= 1 & x = PFArt (m,k) ) or x = PFCrt (1,k) ) by A1, Def4;
suppose ex m being non empty Element of NAT st
( m <= 1 & x = PFArt (m,k) ) ; ::_thesis: x in {(PFArt (1,k)),(PFCrt (1,k))}
then consider m being non empty Element of NAT  such that
A2: m <= 1 and
A3: x = PFArt (m,k) ;
 m >= 1 by NAT_1:14;
then  m = 1 by A2, XXREAL_0:1;
hence  x in {(PFArt (1,k)),(PFCrt (1,k))} by A3, TARSKI:def_2; ::_thesis: verum
end;
suppose x = PFCrt (1,k) ; ::_thesis: x in {(PFArt (1,k)),(PFCrt (1,k))}
hence  x in {(PFArt (1,k)),(PFCrt (1,k))} by TARSKI:def_2; ::_thesis: verum
end;
end;
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(PFArt (1,k)),(PFCrt (1,k))} or x in PFBrt (1,k) )
assume A4: x in {(PFArt (1,k)),(PFCrt (1,k))} ; ::_thesis: x in PFBrt (1,k)
percases ( x = PFArt (1,k) or x = PFCrt (1,k) ) by A4, TARSKI:def_2;
suppose x = PFArt (1,k) ; ::_thesis: x in PFBrt (1,k)
hence  x in PFBrt (1,k) by Def4; ::_thesis: verum
end;
suppose x = PFCrt (1,k) ; ::_thesis: x in PFBrt (1,k)
hence  x in PFBrt (1,k) by Def4; ::_thesis: verum
end;
end;
end;

theorem Th27: :: HEYTING3:27
for k being Element of NAT holds PFBrt (1,k) <> {{}}
proof
let k be Element of NAT ; ::_thesis: PFBrt (1,k) <> {{}}
 PFArt (1,k) in PFBrt (1,k) by Def4;
hence  PFBrt (1,k) <> {{}} by TARSKI:def_1; ::_thesis: verum
end;

registration
let k be Element of NAT ;
cluster PFBrt (1,k) ->  non empty ;
coherence
 not PFBrt (1,k) is empty
proof
 PFArt (1,k) in PFBrt (1,k) by Def4;
hence  not PFBrt (1,k) is empty ; ::_thesis: verum
end;
end;

theorem Th28: :: HEYTING3:28
for n, k being Element of NAT holds {(PFArt (n,k))} is Element of (SubstPoset (NAT,{k}))
proof
let n, k be Element of NAT ; ::_thesis: {(PFArt (n,k))} is Element of (SubstPoset (NAT,{k}))
 SubstitutionSet (NAT,{k}) = the carrier of (SubstPoset (NAT,{k})) by SUBSTLAT:def_4;
hence  {(PFArt (n,k))} is Element of (SubstPoset (NAT,{k})) by HEYTING2:2; ::_thesis: verum
end;

theorem Th29: :: HEYTING3:29
for k being Element of NAT
for V, X being set
for a being Element of (SubstPoset (V,{k})) st X in a holds
X is finite Subset of [:V,{k}:]
proof
let k be Element of NAT ; ::_thesis: for V, X being set
for a being Element of (SubstPoset (V,{k})) st X in a holds
X is finite Subset of [:V,{k}:]
let V, X be set ; ::_thesis: for a being Element of (SubstPoset (V,{k})) st X in a holds
X is finite Subset of [:V,{k}:]
let a be Element of (SubstPoset (V,{k})); ::_thesis: ( X in a implies X is finite Subset of [:V,{k}:] )
assume A1: X in a ; ::_thesis: X is finite Subset of [:V,{k}:]
A2: PFuncs (V,{k}) c= bool [:V,{k}:] by PRE_POLY:16;
A3: SubstitutionSet (V,{k}) = the carrier of (SubstPoset (V,{k})) by SUBSTLAT:def_4;
then  a in SubstitutionSet (V,{k}) ;
then  a c= PFuncs (V,{k}) by FINSUB_1:def_5;
then  X in PFuncs (V,{k}) by A1;
hence  X is finite Subset of [:V,{k}:] by A3, A1, A2, HEYTING2:1; ::_thesis: verum
end;

theorem Th30: :: HEYTING3:30
for m being Element of NAT
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 & not n is odd )
proof
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 & not n is odd )
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 & not n is odd ) )
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 & not n is odd )
let X be non empty set ; ::_thesis: ( X in a implies ex n being Element of NAT st
( [n,m] in X & not n is odd ) )
assume A2: X in a ; ::_thesis: ex n being Element of NAT st
( [n,m] in X & not n is odd )
then reconsider X9 = X as non empty finite Subset of [:NAT,{m}:] by Th29;
assume A3: for n being Element of NAT st [n,m] in X holds
n is odd ; ::_thesis: contradiction
A4: now__::_thesis:_for_k_being_non_empty_Element_of_NAT_holds_[((2_*_k)_+_1),m]_in_X
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 Th25;
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, Th12;
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 Th4;
hence  contradiction by A4; ::_thesis: verum
end;

theorem Th31: :: HEYTING3:31
for k being Element of NAT
for a, b being Element of (SubstPoset (NAT,{k}))
for X being Subset of (SubstPoset (NAT,{k})) st a is_<=_than X & b is_<=_than X holds
a "\/" b is_<=_than X
proof
let k be Element of NAT ; ::_thesis: for a, b being Element of (SubstPoset (NAT,{k}))
for X being Subset of (SubstPoset (NAT,{k})) st a is_<=_than X & b is_<=_than X holds
a "\/" b is_<=_than X
let a, b be Element of (SubstPoset (NAT,{k})); ::_thesis: for X being Subset of (SubstPoset (NAT,{k})) st a is_<=_than X & b is_<=_than X holds
a "\/" b is_<=_than X
let X be Subset of (SubstPoset (NAT,{k})); ::_thesis: ( a is_<=_than X & b is_<=_than X implies a "\/" b is_<=_than X )
assume A1: ( a is_<=_than X & b is_<=_than X ) ; ::_thesis: a "\/" b is_<=_than X
let c be Element of (SubstPoset (NAT,{k})); :: according to LATTICE3:def_8 ::_thesis: ( not c in X or a "\/" b <= c )
assume  c in X ; ::_thesis: a "\/" b <= c
then  ( a <= c & b <= c ) by A1, LATTICE3:def_8;
hence  a "\/" b <= c by YELLOW_5:9; ::_thesis: verum
end;

registration
let k be Element of NAT ;
cluster non empty for Element of the carrier of (SubstPoset (NAT,{k}));
existence
 not for b1 being Element of (SubstPoset (NAT,{k})) holds b1 is empty
proof
 SubstitutionSet (NAT,{k}) = the carrier of (SubstPoset (NAT,{k})) by SUBSTLAT:def_4;
then reconsider E = {{}} as Element of (SubstPoset (NAT,{k})) by SUBSTLAT:2;
take  E ; ::_thesis: not E is empty
thus  not E is empty ; ::_thesis: verum
end;
end;

Lm9:  for a being non empty set st a <> {{}} & {} in a holds
ex b being set st
( b in a & b <> {} )
proof
let a be non empty set ; ::_thesis: ( a <> {{}} & {} in a implies ex b being set st
( b in a & b <> {} ) )
assume that
A1: a <> {{}} and
A2: {} in a ; ::_thesis: ex b being set st
( b in a & b <> {} )
assume A3: for b being set st b in a holds
b = {} ; ::_thesis: contradiction
 a = {{}}
proof
thus  a c= {{}} :: according to XBOOLE_0:def_10 ::_thesis: {{}} c= a
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in a or x in {{}} )
assume  x in a ; ::_thesis: x in {{}}
then  x = {} by A3;
hence  x in {{}} by TARSKI:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {{}} or x in a )
assume  x in {{}} ; ::_thesis: x in a
hence  x in a by A2, TARSKI:def_1; ::_thesis: verum
end;
hence  contradiction by A1; ::_thesis: verum
end;

theorem Th32: :: HEYTING3:32
for n being Element of NAT
for a being Element of (SubstPoset (NAT,{n})) st {} in a holds
a = {{}}
proof
let n be Element of NAT ; ::_thesis: for a being Element of (SubstPoset (NAT,{n})) st {} in a holds
a = {{}}
let a be Element of (SubstPoset (NAT,{n})); ::_thesis: ( {} in a implies a = {{}} )
assume A1: {} in a ; ::_thesis: a = {{}}
 SubstitutionSet (NAT,{n}) = the carrier of (SubstPoset (NAT,{n})) by SUBSTLAT:def_4;
then A2: a in SubstitutionSet (NAT,{n}) ;
assume  a <> {{}} ; ::_thesis: contradiction
then  ex k being set st
( k in a & k <> {} ) by A1, Lm9;
hence  contradiction by A2, A1, SUBSTLAT:5, XBOOLE_1:2; ::_thesis: verum
end;

theorem Th33: :: HEYTING3:33
for k being Element of NAT
for a being non empty Element of (SubstPoset (NAT,{k})) st a <> {{}} holds
ex f being finite Function st
( f in a & f <> {} )
proof
let k be Element of NAT ; ::_thesis: for a being non empty Element of (SubstPoset (NAT,{k})) st a <> {{}} holds
ex f being finite Function st
( f in a & f <> {} )
let a be non empty Element of (SubstPoset (NAT,{k})); ::_thesis: ( a <> {{}} implies ex f being finite Function st
( f in a & f <> {} ) )
assume A1: a <> {{}} ; ::_thesis: ex f being finite Function st
( f in a & f <> {} )
consider f being set  such that
A2: f in a by XBOOLE_0:def_1;
 SubstitutionSet (NAT,{k}) = the carrier of (SubstPoset (NAT,{k})) by SUBSTLAT:def_4;
then reconsider f = f as finite Function by A2, HEYTING2:1;
take  f ; ::_thesis: ( f in a & f <> {} )
thus  f in a by A2; ::_thesis: f <> {}
assume  f = {} ; ::_thesis: contradiction
hence  contradiction by A1, A2, Th32; ::_thesis: verum
end;

theorem Th34: :: HEYTING3:34
for k being Element of NAT
for a being non empty Element of (SubstPoset (NAT,{k}))
for a9 being Element of Fin (PFuncs (NAT,{k})) st a <> {{}} & a = a9 holds
Involved a9 is non empty finite Subset of NAT
proof
let k be Element of NAT ; ::_thesis: for a being non empty Element of (SubstPoset (NAT,{k}))
for a9 being Element of Fin (PFuncs (NAT,{k})) st a <> {{}} & a = a9 holds
Involved a9 is non empty finite Subset of NAT
let a be non empty Element of (SubstPoset (NAT,{k})); ::_thesis: for a9 being Element of Fin (PFuncs (NAT,{k})) st a <> {{}} & a = a9 holds
Involved a9 is non empty finite Subset of NAT
let a9 be Element of Fin (PFuncs (NAT,{k})); ::_thesis: ( a <> {{}} & a = a9 implies Involved a9 is non empty finite Subset of NAT )
assume that
A1: a <> {{}} and
A2: a = a9 ; ::_thesis: Involved a9 is non empty finite Subset of NAT
consider f being finite Function such that
A3: f in a and
A4: f <> {} by A1, Th33;
 ex k1 being set st k1 in dom f by A4, XBOOLE_0:def_1;
hence  Involved a9 is non empty finite Subset of NAT by A2, A3, HEYTING2:6, HEYTING2:def_1; ::_thesis: verum
end;

theorem Th35: :: HEYTING3:35
for k being Element of NAT
for a being Element of (SubstPoset (NAT,{k}))
for a9 being Element of Fin (PFuncs (NAT,{k}))
for B being non empty finite Subset of NAT st B = Involved a9 & a9 = a holds
for X being set st X in a holds
for l being Element of NAT st l > (max B) + 1 holds
not [l,k] in X
proof
let k be Element of NAT ; ::_thesis: for a being Element of (SubstPoset (NAT,{k}))
for a9 being Element of Fin (PFuncs (NAT,{k}))
for B being non empty finite Subset of NAT st B = Involved a9 & a9 = a holds
for X being set st X in a holds
for l being Element of NAT st l > (max B) + 1 holds
not [l,k] in X
let a be Element of (SubstPoset (NAT,{k})); ::_thesis: for a9 being Element of Fin (PFuncs (NAT,{k}))
for B being non empty finite Subset of NAT st B = Involved a9 & a9 = a holds
for X being set st X in a holds
for l being Element of NAT st l > (max B) + 1 holds
not [l,k] in X
let a9 be Element of Fin (PFuncs (NAT,{k})); ::_thesis: for B being non empty finite Subset of NAT st B = Involved a9 & a9 = a holds
for X being set st X in a holds
for l being Element of NAT st l > (max B) + 1 holds
not [l,k] in X
let B be non empty finite Subset of NAT; ::_thesis: ( B = Involved a9 & a9 = a implies for X being set st X in a holds
for l being Element of NAT st l > (max B) + 1 holds
not [l,k] in X )
assume that
A1: B = Involved a9 and
A2: a9 = a ; ::_thesis: for X being set st X in a holds
for l being Element of NAT st l > (max B) + 1 holds
not [l,k] in X
let X be set ; ::_thesis: ( X in a implies for l being Element of NAT st l > (max B) + 1 holds
not [l,k] in X )
assume A3: X in a ; ::_thesis: for l being Element of NAT st l > (max B) + 1 holds
not [l,k] in X
 SubstitutionSet (NAT,{k}) = the carrier of (SubstPoset (NAT,{k})) by SUBSTLAT:def_4;
then reconsider X9 = X as finite Function by A3, HEYTING2:1;
let l be Element of NAT ; ::_thesis: ( l > (max B) + 1 implies not [l,k] in X )
assume A4: l > (max B) + 1 ; ::_thesis: not [l,k] in X
assume  [l,k] in X ; ::_thesis: contradiction
then  l in dom X9 by XTUPLE_0:def_12;
then  l in Involved a9 by A2, A3, HEYTING2:def_1;
then  ( (max B) + 1 >= max B & max B >= l ) by A1, NAT_1:11, XXREAL_2:def_8;
hence  contradiction by A4, XXREAL_0:2; ::_thesis: verum
end;

theorem Th36: :: HEYTING3:36
for k being Element of NAT holds Top (SubstPoset (NAT,{k})) = {{}}
proof
let k be Element of NAT ; ::_thesis: Top (SubstPoset (NAT,{k})) = {{}}
 SubstitutionSet (NAT,{k}) = the carrier of (SubstPoset (NAT,{k})) by SUBSTLAT:def_4;
then reconsider a = {{}} as Element of (SubstPoset (NAT,{k})) by SUBSTLAT:2;
A1: for b being Element of (SubstPoset (NAT,{k})) st b is_<=_than {} holds
a >= b
proof
let b be Element of (SubstPoset (NAT,{k})); ::_thesis: ( b is_<=_than {} implies a >= b )
assume  b is_<=_than {} ; ::_thesis: a >= b
now__::_thesis:_for_x_being_set_st_x_in_b_holds_
ex_y_being_set_st_
(_y_in_a_&_y_c=_x_)
let x be set ; ::_thesis: ( x in b implies ex y being set st
( y in a & y c= x ) )
assume  x in b ; ::_thesis: ex y being set st
( y in a & y c= x )
take y = {} ; ::_thesis: ( y in a & y c= x )
thus  ( y in a & y c= x ) by TARSKI:def_1, XBOOLE_1:2; ::_thesis: verum
end;
hence  a >= b by Th12; ::_thesis: verum
end;
 a is_<=_than {} by YELLOW_0:6;
then  a = "/\" ({},(SubstPoset (NAT,{k}))) by A1, YELLOW_0:31;
hence  Top (SubstPoset (NAT,{k})) = {{}} by YELLOW_0:def_12; ::_thesis: verum
end;

theorem Th37: :: HEYTING3:37
for k being Element of NAT holds Bottom (SubstPoset (NAT,{k})) = {}
proof
let k be Element of NAT ; ::_thesis: Bottom (SubstPoset (NAT,{k})) = {}
 SubstitutionSet (NAT,{k}) = the carrier of (SubstPoset (NAT,{k})) by SUBSTLAT:def_4;
then reconsider a = {} as Element of (SubstPoset (NAT,{k})) by SUBSTLAT:1;
A1: for b being Element of (SubstPoset (NAT,{k})) st b is_>=_than {} holds
a <= b
proof
let b be Element of (SubstPoset (NAT,{k})); ::_thesis: ( b is_>=_than {} implies a <= b )
assume  b is_>=_than {} ; ::_thesis: a <= b
 for x being set st x in a holds
ex y being set st
( y in b & y c= x ) ;
hence  a <= b by Th12; ::_thesis: verum
end;
 a is_>=_than {} by YELLOW_0:6;
then  a = "\/" ({},(SubstPoset (NAT,{k}))) by A1, YELLOW_0:30;
hence  Bottom (SubstPoset (NAT,{k})) = {} by YELLOW_0:def_11; ::_thesis: verum
end;

theorem Th38: :: HEYTING3:38
for k being Element of NAT
for a, b being Element of (SubstPoset (NAT,{k})) st a <= b & a = {{}} holds
b = {{}}
proof
let k be Element of NAT ; ::_thesis: for a, b being Element of (SubstPoset (NAT,{k})) st a <= b & a = {{}} holds
b = {{}}
let a, b be Element of (SubstPoset (NAT,{k})); ::_thesis: ( a <= b & a = {{}} implies b = {{}} )
assume A1: ( a <= b & a = {{}} ) ; ::_thesis: b = {{}}
 Top (SubstPoset (NAT,{k})) = {{}} by Th36;
hence  b = {{}} by A1, WAYBEL15:3; ::_thesis: verum
end;

theorem Th39: :: HEYTING3:39
for k being Element of NAT
for a, b being Element of (SubstPoset (NAT,{k})) st a <= b & b = {} holds
a = {}
proof
let k be Element of NAT ; ::_thesis: for a, b being Element of (SubstPoset (NAT,{k})) st a <= b & b = {} holds
a = {}
let a, b be Element of (SubstPoset (NAT,{k})); ::_thesis: ( a <= b & b = {} implies a = {} )
assume A1: ( a <= b & b = {} ) ; ::_thesis: a = {}
 Bottom (SubstPoset (NAT,{k})) = {} by Th37;
hence  a = {} by A1, YELLOW_5:19; ::_thesis: verum
end;

theorem Th40: :: HEYTING3:40
for m being Element of NAT
for a being Element of (SubstPoset (NAT,{m})) st PFDrt m is_>=_than a holds
a <> {{}}
proof
let m be Element of NAT ; ::_thesis: for a being Element of (SubstPoset (NAT,{m})) st PFDrt m is_>=_than a holds
a <> {{}}
reconsider P1 = PFBrt (1,m) as Element of (SubstPoset (NAT,{m})) by Th25;
let a be Element of (SubstPoset (NAT,{m})); ::_thesis: ( PFDrt m is_>=_than a implies a <> {{}} )
assume A1: PFDrt m is_>=_than a ; ::_thesis: a <> {{}}
 PFBrt (1,m) in PFDrt m by Def5;
then A2: P1 >= a by A1, LATTICE3:def_8;
assume A3: a = {{}} ; ::_thesis: contradiction
 Top (SubstPoset (NAT,{m})) = {{}} by Th36;
hence  contradiction by A3, A2, Th27, WAYBEL15:3; ::_thesis: verum
end;

Lm10:  for m being Element of NAT holds not SubstPoset (NAT,{m}) is complete
proof
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 empty 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 empty 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 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;
percases ( n < mX or n >= mX ) ;
supposeA8: 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;
supposeA9: 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;
percases ( 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
percases ( 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;
supposeA18: 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, LATTICE3:def_8;
 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
end;

registration
let m be Element of NAT ;
cluster SubstPoset (NAT,{m}) ->  non complete ;
coherence
 not SubstPoset (NAT,{m}) is complete by Lm10;
end;

registration
let m be Element of NAT ;
cluster SubstLatt (NAT,{m}) ->  non complete ;
coherence
 not SubstLatt (NAT,{m}) is complete
proof
assume  SubstLatt (NAT,{m}) is complete ; ::_thesis: contradiction
then reconsider K = SubstLatt (NAT,{m}) as complete Lattice ;
 ( LattPOSet K is complete & not SubstPoset (NAT,{m}) is complete ) ;
hence  contradiction ; ::_thesis: verum
end;
end;