:: HEYTING2 semantic presentation

begin


theorem Th1: :: HEYTING2:1
for V, C, a, b being set st b in SubstitutionSet (V,C) & a in b holds
a is finite Function
proof
let V, C be set ; ::_thesis: for a, b being set st b in SubstitutionSet (V,C) & a in b holds
a is finite Function
let a, b be set ; ::_thesis: ( b in SubstitutionSet (V,C) & a in b implies a is finite Function )
assume that
A1: b in SubstitutionSet (V,C) and
A2: a in b ; ::_thesis: a is finite Function
 b in  {  A where A is Element of Fin (PFuncs (V,C)) : ( ( for u being set st u in A holds
u is finite ) & ( for s1, t being Element of PFuncs (V,C) st s1 in A & t in A & s1 c= t holds
s1 = t ) )  }  by A1, SUBSTLAT:def_1;
then  ex A being Element of Fin (PFuncs (V,C)) st
( A = b & ( 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 ) ) ;
hence  a is finite Function by A1, A2; ::_thesis: verum
end;

Lm1:  for A, B, C being set st A = B \/ C & A c= B holds
A = B
proof
let A, B, C be set ; ::_thesis: ( A = B \/ C & A c= B implies A = B )
assume that
A1: A = B \/ C and
A2: A c= B ; ::_thesis: A = B
 B c= A by A1, XBOOLE_1:7;
hence  A = B by A2, XBOOLE_0:def_10; ::_thesis: verum
end;

begin

theorem Th2: :: HEYTING2:2
for V, C being set
for a being finite Element of PFuncs (V,C) holds {a} in SubstitutionSet (V,C)
proof
let V, C be set ; ::_thesis: for a being finite Element of PFuncs (V,C) holds {a} in SubstitutionSet (V,C)
let a be finite Element of PFuncs (V,C); ::_thesis: {a} in SubstitutionSet (V,C)
A1: for s, t being Element of PFuncs (V,C) st s in {a} & t in {a} & s c= t holds
s = t
proof
let s, t be Element of PFuncs (V,C); ::_thesis: ( s in {a} & t in {a} & s c= t implies s = t )
assume that
A2: s in {a} and
A3: t in {a} and
 s c= t ; ::_thesis: s = t
 s = a by A2, TARSKI:def_1;
hence  s = t by A3, TARSKI:def_1; ::_thesis: verum
end;
 for u being set st u in {a} holds
u is finite ;
then  {.a.} 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 A1;
hence  {a} in SubstitutionSet (V,C) by SUBSTLAT:def_1; ::_thesis: verum
end;

theorem :: HEYTING2:3
for V, C being set
for A, B being Element of SubstitutionSet (V,C) st A ^ B = A holds
for a being set st a in A holds
ex b being set st
( b in B & b c= a )
proof
let V, C be set ; ::_thesis: for A, B being Element of SubstitutionSet (V,C) st A ^ B = A holds
for a being set st a in A holds
ex b being set st
( b in B & b c= a )
let A, B be Element of SubstitutionSet (V,C); ::_thesis: ( A ^ B = A implies for a being set st a in A holds
ex b being set st
( b in B & b c= a ) )
assume A1: A ^ B = A ; ::_thesis: for a being set st a in A holds
ex b being set st
( b in B & b c= a )
let a be set ; ::_thesis: ( a in A implies ex b being set st
( b in B & b c= a ) )
assume  a in A ; ::_thesis: ex b being set st
( b in B & b c= a )
then consider b, c being set  such that
 b in A and
A2: c in B and
A3: a = b \/ c by A1, SUBSTLAT:15;
take  c ; ::_thesis: ( c in B & c c= a )
thus  ( c in B & c c= a ) by A2, A3, XBOOLE_1:7; ::_thesis: verum
end;

theorem Th4: :: HEYTING2:4
for V, C being set
for A, B being Element of SubstitutionSet (V,C) st mi (A ^ B) = A holds
for a being set st a in A holds
ex b being set st
( b in B & b c= a )
proof
let V, C be set ; ::_thesis: for A, B being Element of SubstitutionSet (V,C) st mi (A ^ B) = A holds
for a being set st a in A holds
ex b being set st
( b in B & b c= a )
let A, B be Element of SubstitutionSet (V,C); ::_thesis: ( mi (A ^ B) = A implies for a being set st a in A holds
ex b being set st
( b in B & b c= a ) )
assume A1: mi (A ^ B) = A ; ::_thesis: for a being set st a in A holds
ex b being set st
( b in B & b c= a )
let a be set ; ::_thesis: ( a in A implies ex b being set st
( b in B & b c= a ) )
A2: mi (A ^ B) c= A ^ B by SUBSTLAT:8;
assume  a in A ; ::_thesis: ex b being set st
( b in B & b c= a )
then consider b, c being set  such that
 b in A and
A3: c in B and
A4: a = b \/ c by A1, A2, SUBSTLAT:15;
take  c ; ::_thesis: ( c in B & c c= a )
thus  ( c in B & c c= a ) by A3, A4, XBOOLE_1:7; ::_thesis: verum
end;

theorem Th5: :: HEYTING2:5
for V, C being set
for A, B being Element of SubstitutionSet (V,C) st ( for a being set st a in A holds
ex b being set st
( b in B & b c= a ) ) holds
mi (A ^ B) = A
proof
let V, C be set ; ::_thesis: for A, B being Element of SubstitutionSet (V,C) st ( for a being set st a in A holds
ex b being set st
( b in B & b c= a ) ) holds
mi (A ^ B) = A
let A, B be Element of SubstitutionSet (V,C); ::_thesis: ( ( for a being set st a in A holds
ex b being set st
( b in B & b c= a ) ) implies mi (A ^ B) = A )
assume A1: for a being set st a in A holds
ex b being set st
( b in B & b c= a ) ; ::_thesis: mi (A ^ B) = A
A2: mi (A ^ B) c= A ^ B by SUBSTLAT:8;
thus  mi (A ^ B) c= A :: according to XBOOLE_0:def_10 ::_thesis: A c= mi (A ^ B)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in mi (A ^ B) or a in A )
A3: A c= PFuncs (V,C) by FINSUB_1:def_5;
assume A4: a in mi (A ^ B) ; ::_thesis: a in A
then consider b, c being set  such that
A5: b in A and
 c in B and
A6: a = b \/ c by A2, SUBSTLAT:15;
A7: b c= a by A6, XBOOLE_1:7;
consider b1 being set  such that
A8: b1 in B and
A9: b1 c= b by A1, A5;
 B c= PFuncs (V,C) by FINSUB_1:def_5;
then reconsider b9 = b, b19 = b1 as Element of PFuncs (V,C) by A5, A8, A3;
A10: b = b1 \/ b by A9, XBOOLE_1:12;
 b19 tolerates b9 by A9, PARTFUN1:54;
then  b in A ^ B by A5, A8, A10, SUBSTLAT:16;
hence  a in A by A4, A5, A7, SUBSTLAT:6; ::_thesis: verum
end;
thus  A c= mi (A ^ B) ::_thesis: verum
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in A or a in mi (A ^ B) )
A11: A c= PFuncs (V,C) by FINSUB_1:def_5;
assume A12: a in A ; ::_thesis: a in mi (A ^ B)
then consider b being set  such that
A13: b in B and
A14: b c= a by A1;
 B c= PFuncs (V,C) by FINSUB_1:def_5;
then reconsider a9 = a, b9 = b as Element of PFuncs (V,C) by A12, A13, A11;
A15: a9 tolerates b9 by A14, PARTFUN1:54;
A16: a in mi A by A12, SUBSTLAT:11;
A17: for b being finite set st b in A ^ B & b c= a holds
b = a
proof
let b be finite set ; ::_thesis: ( b in A ^ B & b c= a implies b = a )
assume that
A18: b in A ^ B and
A19: b c= a ; ::_thesis: b = a
consider c, d being set  such that
A20: c in A and
 d in B and
A21: b = c \/ d by A18, SUBSTLAT:15;
 c c= b by A21, XBOOLE_1:7;
then  c c= a by A19, XBOOLE_1:1;
then  c = a by A16, A20, SUBSTLAT:6;
hence  b = a by A19, A21, Lm1; ::_thesis: verum
end;
 a9 = a9 \/ b9 by A14, XBOOLE_1:12;
then A22: a9 in A ^ B by A12, A13, A15, SUBSTLAT:16;
 a is finite by A12, Th1;
hence  a in mi (A ^ B) by A22, A17, SUBSTLAT:7; ::_thesis: verum
end;
end;

definition
let V be set ;
let C be finite set ;
let A be Element of Fin (PFuncs (V,C));
func Involved A ->  set  means :Def1: :: HEYTING2:def 1
 for x being set holds
( x in it iff ex f being finite Function st
( f in A & x in dom f ) );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff ex f being finite Function st
( f in A & x in dom f ) )
proof
defpred S1[ set ] means  ex f being finite Function st
( f in A & $1 in dom f );
consider X being set  such that
A1: for x being set holds
( x in X iff ( x in V & S1[x] ) ) from XBOOLE_0:sch_1();
take  X ; ::_thesis: for x being set holds
( x in X iff ex f being finite Function st
( f in A & x in dom f ) )
let x be set ; ::_thesis: ( x in X iff ex f being finite Function st
( f in A & x in dom f ) )
thus  ( x in X implies ex f being finite Function st
( f in A & x in dom f ) ) by A1; ::_thesis: ( ex f being finite Function st
( f in A & x in dom f ) implies x in X )
given f being finite Function such that A2: f in A and
A3: x in dom f ; ::_thesis: x in X
 A c= PFuncs (V,C) by FINSUB_1:def_5;
then  ex f1 being Function st
( f = f1 & dom f1 c= V & rng f1 c= C ) by A2, PARTFUN1:def_3;
hence  x in X by A1, A2, A3; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff ex f being finite Function st
( f in A & x in dom f ) ) ) & ( for x being set holds
( x in b2 iff ex f being finite Function st
( f in A & x in dom f ) ) ) holds
b1 = b2
proof
defpred S1[ set ] means  ex f being finite Function st
( f in A & $1 in dom f );
let r, s be set ; ::_thesis: ( ( for x being set holds
( x in r iff ex f being finite Function st
( f in A & x in dom f ) ) ) & ( for x being set holds
( x in s iff ex f being finite Function st
( f in A & x in dom f ) ) ) implies r = s )
assume that
A4: for x being set holds
( x in r iff ex f being finite Function st
( f in A & x in dom f ) ) and
A5: for x being set holds
( x in s iff ex f being finite Function st
( f in A & x in dom f ) ) ; ::_thesis: r = s
 for X1, X2 being set 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 XBOOLE_0:sch_3();
hence  r = s by A4, A5; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines Involved HEYTING2:def_1_:_
 for V being set
for C being finite set
for A being Element of Fin (PFuncs (V,C))
for b4 being set holds
( b4 = Involved A iff for x being set holds
( x in b4 iff ex f being finite Function st
( f in A & x in dom f ) ) );

theorem Th6: :: HEYTING2:6
for V being set
for C being finite set
for A being Element of Fin (PFuncs (V,C)) holds Involved A c= V
proof
let V be set ; ::_thesis: for C being finite set
for A being Element of Fin (PFuncs (V,C)) holds Involved A c= V
let C be finite set ; ::_thesis: for A being Element of Fin (PFuncs (V,C)) holds Involved A c= V
let A be Element of Fin (PFuncs (V,C)); ::_thesis: Involved A c= V
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Involved A or a in V )
assume  a in Involved A ; ::_thesis: a in V
then consider f being finite Function such that
A1: f in A and
A2: a in dom f by Def1;
 A c= PFuncs (V,C) by FINSUB_1:def_5;
then  ex f1 being Function st
( f = f1 & dom f1 c= V & rng f1 c= C ) by A1, PARTFUN1:def_3;
hence  a in V by A2; ::_thesis: verum
end;

Lm2:  for V being set
for C being finite set
for A being non empty Element of Fin (PFuncs (V,C)) holds Involved A is finite
proof
deffunc H1( Function) ->  set = dom $1;
let V be set ; ::_thesis: for C being finite set
for A being non empty Element of Fin (PFuncs (V,C)) holds Involved A is finite
let C be finite set ; ::_thesis: for A being non empty Element of Fin (PFuncs (V,C)) holds Involved A is finite
let A be non empty Element of Fin (PFuncs (V,C)); ::_thesis: Involved A is finite
defpred S1[ set ] means ( $1 in A & $1 is finite );
defpred S2[ set ] means $1 in A;
set X =  {  H1(f) where f is Element of PFuncs (V,C) : S1[f]  }  ;
A1: for x being set st x in  {  H1(f) where f is Element of PFuncs (V,C) : S1[f]  }  holds
x is finite
proof
let x be set ; ::_thesis: ( x in  {  H1(f) where f is Element of PFuncs (V,C) : S1[f]  }  implies x is finite )
assume  x in  {  H1(f) where f is Element of PFuncs (V,C) : S1[f]  }  ; ::_thesis: x is finite
then  ex f1 being Element of PFuncs (V,C) st
( x = dom f1 & f1 in A & f1 is finite ) ;
hence  x is finite ; ::_thesis: verum
end;
A2: A is finite ;
A3:  {  H1(f) where f is Element of PFuncs (V,C) : f in A  }  is finite from FRAENKEL:sch_21(A2);
 for x being set holds
( x in Involved A iff ex Y being set st
( x in Y & Y in  {  H1(f) where f is Element of PFuncs (V,C) : S1[f]  }  ) )
proof
let x be set ; ::_thesis: ( x in Involved A iff ex Y being set st
( x in Y & Y in  {  H1(f) where f is Element of PFuncs (V,C) : S1[f]  }  ) )
hereby  ::_thesis: ( ex Y being set st
( x in Y & Y in  {  H1(f) where f is Element of PFuncs (V,C) : S1[f]  }  ) implies x in Involved A )
assume  x in Involved A ; ::_thesis: ex Y being set st
( x in Y & Y in  {  H1(f) where f is Element of PFuncs (V,C) : S1[f]  }  )
then consider f being finite Function such that
A4: f in A and
A5: x in dom f by Def1;
 A c= PFuncs (V,C) by FINSUB_1:def_5;
then  dom f in  {  H1(f) where f is Element of PFuncs (V,C) : S1[f]  }  by A4;
hence  ex Y being set st
( x in Y & Y in  {  H1(f) where f is Element of PFuncs (V,C) : S1[f]  }  ) by A5; ::_thesis: verum
end;
given Y being set  such that A6: x in Y and
A7: Y in  {  H1(f) where f is Element of PFuncs (V,C) : S1[f]  }  ; ::_thesis: x in Involved A
 ex f1 being Element of PFuncs (V,C) st
( Y = dom f1 & f1 in A & f1 is finite ) by A7;
hence  x in Involved A by A6, Def1; ::_thesis: verum
end;
then A8: Involved A = union  {  H1(f) where f is Element of PFuncs (V,C) : S1[f]  }  by TARSKI:def_4;
A9: for g being Element of PFuncs (V,C) st S1[g] holds
S2[g] ;
  {  H1(f) where f is Element of PFuncs (V,C) : S1[f]  }  c=  {  H1(f) where f is Element of PFuncs (V,C) : S2[f]  }  from FRAENKEL:sch_1(A9);
hence  Involved A is finite by A3, A8, A1, FINSET_1:7; ::_thesis: verum
end;

theorem Th7: :: HEYTING2:7
for V being set
for C being finite set
for A being Element of Fin (PFuncs (V,C)) st A = {} holds
Involved A = {}
proof
let V be set ; ::_thesis: for C being finite set
for A being Element of Fin (PFuncs (V,C)) st A = {} holds
Involved A = {}
let C be finite set ; ::_thesis: for A being Element of Fin (PFuncs (V,C)) st A = {} holds
Involved A = {}
let A be Element of Fin (PFuncs (V,C)); ::_thesis: ( A = {} implies Involved A = {} )
assume A1: A = {} ; ::_thesis: Involved A = {}
assume  Involved A <> {} ; ::_thesis: contradiction
then consider x being set  such that
A2: x in Involved A by XBOOLE_0:def_1;
 ex f being finite Function st
( f in A & x in dom f ) by A2, Def1;
hence  contradiction by A1; ::_thesis: verum
end;

registration
let V be set ;
let C be finite set ;
let A be Element of Fin (PFuncs (V,C));
cluster Involved A ->  finite ;
coherence
 Involved A is finite
proof
percases ( not A is empty or A is empty ) ;
suppose not A is empty ; ::_thesis: Involved A is finite
hence  Involved A is finite by Lm2; ::_thesis: verum
end;
suppose A is empty ; ::_thesis: Involved A is finite
hence  Involved A is finite by Th7; ::_thesis: verum
end;
end;
end;
end;

theorem :: HEYTING2:8
for C being finite set
for A being Element of Fin (PFuncs ({},C)) holds Involved A = {} by Th6, XBOOLE_1:3;

definition
let V be set ;
let C be finite set ;
let A be Element of Fin (PFuncs (V,C));
func - A ->  Element of Fin (PFuncs (V,C)) equals :: HEYTING2:def 2
 {  f where f is Element of PFuncs ((Involved A),C) : for g being Element of PFuncs (V,C) st g in A holds
not f tolerates g  }  ;
coherence
  {  f where f is Element of PFuncs ((Involved A),C) : for g being Element of PFuncs (V,C) st g in A holds
not f tolerates g  }  is Element of Fin (PFuncs (V,C))
proof
deffunc H1( set ) ->  set = $1;
defpred S1[ set ] means verum;
defpred S2[ Element of PFuncs ((Involved A),C)] means  for h being Element of PFuncs (V,C) st h in A holds
not $1 tolerates h;
set M =  {  f where f is Element of PFuncs ((Involved A),C) : for g being Element of PFuncs (V,C) st g in A holds
not f tolerates g  }  ;
A1:  {  f where f is Element of PFuncs ((Involved A),C) : verum  }  c= PFuncs ((Involved A),C)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  f where f is Element of PFuncs ((Involved A),C) : verum  }  or a in PFuncs ((Involved A),C) )
assume  a in  {  f where f is Element of PFuncs ((Involved A),C) : verum  }  ; ::_thesis: a in PFuncs ((Involved A),C)
then  ex f1 being Element of PFuncs ((Involved A),C) st f1 = a ;
hence  a in PFuncs ((Involved A),C) ; ::_thesis: verum
end;
A2: for v being Element of PFuncs ((Involved A),C) st S2[v] holds
S1[v] ;
A3:  {  H1(f) where f is Element of PFuncs ((Involved A),C) : S2[f]  }  c=  {  H1(f) where f is Element of PFuncs ((Involved A),C) : S1[f]  }  from FRAENKEL:sch_1(A2);
A4:  {  f where f is Element of PFuncs ((Involved A),C) : for g being Element of PFuncs (V,C) st g in A holds
not f tolerates g  }  c= PFuncs (V,C)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  f where f is Element of PFuncs ((Involved A),C) : for g being Element of PFuncs (V,C) st g in A holds
not f tolerates g  }  or a in PFuncs (V,C) )
assume  a in  {  f where f is Element of PFuncs ((Involved A),C) : for g being Element of PFuncs (V,C) st g in A holds
not f tolerates g  }  ; ::_thesis: a in PFuncs (V,C)
then  ex f1 being Element of PFuncs ((Involved A),C) st
( f1 = a & ( for g being Element of PFuncs (V,C) st g in A holds
not f1 tolerates g ) ) ;
then A5: a in PFuncs ((Involved A),C) ;
 Involved A c= V by Th6;
then  PFuncs ((Involved A),C) c= PFuncs (V,C) by PARTFUN1:50;
hence  a in PFuncs (V,C) by A5; ::_thesis: verum
end;
 PFuncs ((Involved A),C) is finite by PRE_POLY:17;
hence   {  f where f is Element of PFuncs ((Involved A),C) : for g being Element of PFuncs (V,C) st g in A holds
not f tolerates g  }  is Element of Fin (PFuncs (V,C)) by A3, A1, A4, FINSUB_1:def_5; ::_thesis: verum
end;
end;

:: deftheorem  defines - HEYTING2:def_2_:_
 for V being set
for C being finite set
for A being Element of Fin (PFuncs (V,C)) holds - A =  {  f where f is Element of PFuncs ((Involved A),C) : for g being Element of PFuncs (V,C) st g in A holds
not f tolerates g  }  ;

theorem Th9: :: HEYTING2:9
for V being set
for C being finite set
for A being Element of SubstitutionSet (V,C) holds A ^ (- A) = {}
proof
let V be set ; ::_thesis: for C being finite set
for A being Element of SubstitutionSet (V,C) holds A ^ (- A) = {}
let C be finite set ; ::_thesis: for A being Element of SubstitutionSet (V,C) holds A ^ (- A) = {}
let A be Element of SubstitutionSet (V,C); ::_thesis: A ^ (- A) = {}
assume  A ^ (- A) <> {} ; ::_thesis: contradiction
then consider x being set  such that
A1: x in A ^ (- A) by XBOOLE_0:def_1;
 x in  {  (s \/ t) where s, t is Element of PFuncs (V,C) : ( s in A & t in - A & s tolerates t )  }  by A1, SUBSTLAT:def_3;
then consider s1, t1 being Element of PFuncs (V,C) such that
 x = s1 \/ t1 and
A2: s1 in A and
A3: t1 in - A and
A4: s1 tolerates t1 ;
 ex f1 being Element of PFuncs ((Involved A),C) st
( f1 = t1 & ( for g being Element of PFuncs (V,C) st g in A holds
not f1 tolerates g ) ) by A3;
hence  contradiction by A2, A4; ::_thesis: verum
end;

theorem Th10: :: HEYTING2:10
for V being set
for C being finite set
for A being Element of SubstitutionSet (V,C) st A = {} holds
- A = {{}}
proof
let V be set ; ::_thesis: for C being finite set
for A being Element of SubstitutionSet (V,C) st A = {} holds
- A = {{}}
let C be finite set ; ::_thesis: for A being Element of SubstitutionSet (V,C) st A = {} holds
- A = {{}}
let A be Element of SubstitutionSet (V,C); ::_thesis: ( A = {} implies - A = {{}} )
defpred S1[ Element of PFuncs ((Involved A),C)] means  for g being Element of PFuncs (V,C) st g in A holds
not $1 tolerates g;
assume A1: A = {} ; ::_thesis: - A = {{}}
then A2: for g being Element of PFuncs (V,C) st g in A holds
not {} tolerates g ;
  {  xx where xx is Element of PFuncs ((Involved A),C) : S1[xx]  }  c= PFuncs ((Involved A),C) from FRAENKEL:sch_10();
then  - A c= PFuncs ({},C) by A1, Th7;
then A3: - A c= {{}} by PARTFUN1:48;
 {} in {{}} by TARSKI:def_1;
then  {} in PFuncs ({},C) by PARTFUN1:48;
then  {} in PFuncs ((Involved A),C) by A1, Th7;
then  {} in - A by A2;
then  {{}} c= - A by ZFMISC_1:31;
hence  - A = {{}} by A3, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: HEYTING2:11
for V being set
for C being finite set
for A being Element of SubstitutionSet (V,C) st A = {{}} holds
- A = {}
proof
let V be set ; ::_thesis: for C being finite set
for A being Element of SubstitutionSet (V,C) st A = {{}} holds
- A = {}
let C be finite set ; ::_thesis: for A being Element of SubstitutionSet (V,C) st A = {{}} holds
- A = {}
let A be Element of SubstitutionSet (V,C); ::_thesis: ( A = {{}} implies - A = {} )
assume A1: A = {{}} ; ::_thesis: - A = {}
assume  - A <> {} ; ::_thesis: contradiction
then consider x1 being set  such that
A2: x1 in - A by XBOOLE_0:def_1;
consider f1 being Element of PFuncs ((Involved A),C) such that
 x1 = f1 and
A3: for g being Element of PFuncs (V,C) st g in {{}} holds
not f1 tolerates g by A1, A2;
A4: {} in {{}} by TARSKI:def_1;
 {} is PartFunc of V,C by RELSET_1:12;
then A5: {} in PFuncs (V,C) by PARTFUN1:45;
 f1 tolerates {} by PARTFUN1:59;
hence  contradiction by A3, A5, A4; ::_thesis: verum
end;

theorem Th12: :: HEYTING2:12
for V being set
for C being finite set
for A being Element of SubstitutionSet (V,C) holds mi (A ^ (- A)) = Bottom (SubstLatt (V,C))
proof
let V be set ; ::_thesis: for C being finite set
for A being Element of SubstitutionSet (V,C) holds mi (A ^ (- A)) = Bottom (SubstLatt (V,C))
let C be finite set ; ::_thesis: for A being Element of SubstitutionSet (V,C) holds mi (A ^ (- A)) = Bottom (SubstLatt (V,C))
let A be Element of SubstitutionSet (V,C); ::_thesis: mi (A ^ (- A)) = Bottom (SubstLatt (V,C))
mi (A ^ (- A)) = {} by Th9, SUBSTLAT:9
.= Bottom (SubstLatt (V,C)) by SUBSTLAT:26 ;
hence  mi (A ^ (- A)) = Bottom (SubstLatt (V,C)) ; ::_thesis: verum
end;

theorem :: HEYTING2:13
for V being non empty set
for C being non empty finite set
for A being Element of SubstitutionSet (V,C) st A = {} holds
mi (- A) = Top (SubstLatt (V,C))
proof
let V be non empty set ; ::_thesis: for C being non empty finite set
for A being Element of SubstitutionSet (V,C) st A = {} holds
mi (- A) = Top (SubstLatt (V,C))
let C be non empty finite set ; ::_thesis: for A being Element of SubstitutionSet (V,C) st A = {} holds
mi (- A) = Top (SubstLatt (V,C))
let A be Element of SubstitutionSet (V,C); ::_thesis: ( A = {} implies mi (- A) = Top (SubstLatt (V,C)) )
assume  A = {} ; ::_thesis: mi (- A) = Top (SubstLatt (V,C))
then A1: - A = {{}} by Th10;
then  - A in SubstitutionSet (V,C) by SUBSTLAT:2;
then  mi (- A) = {{}} by A1, SUBSTLAT:11;
hence  mi (- A) = Top (SubstLatt (V,C)) by SUBSTLAT:27; ::_thesis: verum
end;

theorem Th14: :: HEYTING2:14
for V being set
for C being finite set
for A being Element of SubstitutionSet (V,C)
for a being Element of PFuncs (V,C)
for B being Element of SubstitutionSet (V,C) st B = {a} & A ^ B = {} holds
ex b being finite set st
( b in - A & b c= a )
proof
let V be set ; ::_thesis: for C being finite set
for A being Element of SubstitutionSet (V,C)
for a being Element of PFuncs (V,C)
for B being Element of SubstitutionSet (V,C) st B = {a} & A ^ B = {} holds
ex b being finite set st
( b in - A & b c= a )
let C be finite set ; ::_thesis: for A being Element of SubstitutionSet (V,C)
for a being Element of PFuncs (V,C)
for B being Element of SubstitutionSet (V,C) st B = {a} & A ^ B = {} holds
ex b being finite set st
( b in - A & b c= a )
let A be Element of SubstitutionSet (V,C); ::_thesis: for a being Element of PFuncs (V,C)
for B being Element of SubstitutionSet (V,C) st B = {a} & A ^ B = {} holds
ex b being finite set st
( b in - A & b c= a )
let a be Element of PFuncs (V,C); ::_thesis: for B being Element of SubstitutionSet (V,C) st B = {a} & A ^ B = {} holds
ex b being finite set st
( b in - A & b c= a )
let B be Element of SubstitutionSet (V,C); ::_thesis: ( B = {a} & A ^ B = {} implies ex b being finite set st
( b in - A & b c= a ) )
assume A1: B = {a} ; ::_thesis: ( not A ^ B = {} or ex b being finite set st
( b in - A & b c= a ) )
assume A2: A ^ B = {} ; ::_thesis: ex b being finite set st
( b in - A & b c= a )
percases ( not A is empty or A is empty ) ;
supposeA3: not A is empty ; ::_thesis: ex b being finite set st
( b in - A & b c= a )
then reconsider AA = A as non empty finite set ;
defpred S1[ Element of PFuncs (V,C), set ] means ( $2 in (dom $1) /\ (dom a) & $1 . $2 <> a . $2 );
defpred S2[ set ] means verum;
A4: ex kk being Function st
( kk = a & dom kk c= V & rng kk c= C ) by PARTFUN1:def_3;
A5: now__::_thesis:_for_s_being_Element_of_PFuncs_(V,C)_st_s_in_A_holds_
ex_x_being_Element_of_[V]_st_S1[s,x]
let s be Element of PFuncs (V,C); ::_thesis: ( s in A implies ex x being Element of [V] st S1[s,x] )
assume A6: s in A ; ::_thesis: ex x being Element of [V] st S1[s,x]
 not s tolerates a
proof
assume A7: s tolerates a ; ::_thesis: contradiction
 a in B by A1, TARSKI:def_1;
then  s \/ a in  {  (s1 \/ t1) where s1, t1 is Element of PFuncs (V,C) : ( s1 in A & t1 in B & s1 tolerates t1 )  }  by A6, A7;
hence  contradiction by A2, SUBSTLAT:def_3; ::_thesis: verum
end;
then consider x being set  such that
A8: x in (dom s) /\ (dom a) and
A9: s . x <> a . x by PARTFUN1:def_4;
consider a9 being Function such that
A10: a9 = a and
A11: dom a9 c= V and
 rng a9 c= C by PARTFUN1:def_3;
 (dom s) /\ (dom a) c= dom a9 by A10, XBOOLE_1:17;
then  (dom s) /\ (dom a) c= V by A11, XBOOLE_1:1;
then reconsider x = x as Element of [V] by A8, HEYTING1:def_2;
take x = x; ::_thesis: S1[s,x]
thus  S1[s,x] by A8, A9; ::_thesis: verum
end;
consider g being Element of Funcs ((PFuncs (V,C)),[V]) such that
A12: for s being Element of PFuncs (V,C) st s in A holds
S1[s,g . s] from FRAENKEL:sch_27(A5);
deffunc H1( set ) ->  set = g . $1;
A13: A = [A] by A3, HEYTING1:def_2;
  {  H1(b) where b is Element of AA : S2[b]  }  is finite from PRE_CIRC:sch_1();
then reconsider UKA =  {  (g . b) where b is Element of [A] : verum  }  as finite set by A13;
set f = a | UKA;
A14: dom (a | UKA) c= Involved A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom (a | UKA) or x in Involved A )
assume  x in dom (a | UKA) ; ::_thesis: x in Involved A
then  x in UKA by RELAT_1:57;
then consider b being Element of [A] such that
A15: x = g . b ;
reconsider b = b as finite Function by A13, Th1;
reconsider b9 = b as Element of PFuncs (V,C) by A13, SETWISEO:9;
 g . b9 in (dom b9) /\ (dom a) by A13, A12;
then  x in dom b by A15, XBOOLE_0:def_4;
hence  x in Involved A by A13, Def1; ::_thesis: verum
end;
 rng (a | UKA) c= rng a by RELAT_1:70;
then  rng (a | UKA) c= C by A4, XBOOLE_1:1;
then reconsider f9 = a | UKA as Element of PFuncs ((Involved A),C) by A14, PARTFUN1:def_3;
 for g being Element of PFuncs (V,C) st g in A holds
not a | UKA tolerates g
proof
let g1 be Element of PFuncs (V,C); ::_thesis: ( g1 in A implies not a | UKA tolerates g1 )
reconsider g9 = g1 as Function ;
assume A16: g1 in A ; ::_thesis: not a | UKA tolerates g1
 ex z being set st
( z in (dom g1) /\ (dom (a | UKA)) & g9 . z <> (a | UKA) . z )
proof
set z = g . g1;
take  g . g1 ; ::_thesis: ( g . g1 in (dom g1) /\ (dom (a | UKA)) & g9 . (g . g1) <> (a | UKA) . (g . g1) )
A17: g . g1 in (dom g1) /\ (dom a) by A12, A16;
then A18: g . g1 in dom a by XBOOLE_0:def_4;
 g . g1 in  {  (g . b1) where b1 is Element of [A] : verum  }  by A13, A16;
then  g . g1 in (dom a) /\ UKA by A18, XBOOLE_0:def_4;
then A19: g . g1 in dom (a | UKA) by RELAT_1:61;
 g . g1 in dom g1 by A17, XBOOLE_0:def_4;
hence  g . g1 in (dom g1) /\ (dom (a | UKA)) by A19, XBOOLE_0:def_4; ::_thesis: g9 . (g . g1) <> (a | UKA) . (g . g1)
 g1 . (g . g1) <> a . (g . g1) by A12, A16;
hence  g9 . (g . g1) <> (a | UKA) . (g . g1) by A19, FUNCT_1:47; ::_thesis: verum
end;
hence  not a | UKA tolerates g1 by PARTFUN1:def_4; ::_thesis: verum
end;
then  f9 in  {  f1 where f1 is Element of PFuncs ((Involved A),C) : for g being Element of PFuncs (V,C) st g in A holds
not f1 tolerates g  }  ;
hence  ex b being finite set st
( b in - A & b c= a ) by RELAT_1:59; ::_thesis: verum
end;
supposeA20: A is empty ; ::_thesis: ex b being finite set st
( b in - A & b c= a )
reconsider K = {} as finite set ;
take  K ; ::_thesis: ( K in - A & K c= a )
 - A = {{}} by A20, Th10;
hence  ( K in - A & K c= a ) by TARSKI:def_1, XBOOLE_1:2; ::_thesis: verum
end;
end;
end;

definition
let V be set ;
let C be finite set ;
let A, B be Element of Fin (PFuncs (V,C));
funcA =>> B ->  Element of Fin (PFuncs (V,C)) equals :: HEYTING2:def 3
(PFuncs (V,C)) /\  {  (union  {  ((f . i) \ i) where i is Element of PFuncs (V,C) : i in A  }  ) where f is Element of PFuncs (A,B) : dom f = A  }  ;
coherence
 (PFuncs (V,C)) /\  {  (union  {  ((f . i) \ i) where i is Element of PFuncs (V,C) : i in A  }  ) where f is Element of PFuncs (A,B) : dom f = A  }  is Element of Fin (PFuncs (V,C))
proof
reconsider PF = PFuncs (A,B) as functional non empty finite set by PRE_POLY:17;
set Z =  {  (union  {  ((f . i) \ i) where i is Element of PFuncs (V,C) : i in A  }  ) where f is Element of PFuncs (A,B) : dom f = A  }  ;
set K = (PFuncs (V,C)) /\  {  (union  {  ((f . i) \ i) where i is Element of PFuncs (V,C) : i in A  }  ) where f is Element of PFuncs (A,B) : dom f = A  }  ;
A1:  {  (union  {  ((f . i) \ i) where i is Element of PFuncs (V,C) : i in A  }  ) where f is Element of PFuncs (A,B) : dom f = A  }  c=  {  (union  {  ((f . i) \ i) where i is Element of PFuncs (V,C) : i in A  }  ) where f is Element of PFuncs (A,B) : ( f in PFuncs (A,B) & dom f = A )  }
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in  {  (union  {  ((f . i) \ i) where i is Element of PFuncs (V,C) : i in A  }  ) where f is Element of PFuncs (A,B) : dom f = A  }  or z in  {  (union  {  ((f . i) \ i) where i is Element of PFuncs (V,C) : i in A  }  ) where f is Element of PFuncs (A,B) : ( f in PFuncs (A,B) & dom f = A )  }  )
assume  z in  {  (union  {  ((f . i) \ i) where i is Element of PFuncs (V,C) : i in A  }  ) where f is Element of PFuncs (A,B) : dom f = A  }  ; ::_thesis: z in  {  (union  {  ((f . i) \ i) where i is Element of PFuncs (V,C) : i in A  }  ) where f is Element of PFuncs (A,B) : ( f in PFuncs (A,B) & dom f = A )  }
then  ex f1 being Element of PFuncs (A,B) st
( z = union  {  ((f1 . i) \ i) where i is Element of PFuncs (V,C) : i in A  }  & dom f1 = A ) ;
hence  z in  {  (union  {  ((f . i) \ i) where i is Element of PFuncs (V,C) : i in A  }  ) where f is Element of PFuncs (A,B) : ( f in PFuncs (A,B) & dom f = A )  }  ; ::_thesis: verum
end;
defpred S1[ Element of PF] means ( $1 in PFuncs (A,B) & dom $1 = A );
deffunc H1( Element of PF) ->  set = union  {  (($1 . i) \ i) where i is Element of PFuncs (V,C) : i in A  }  ;
A2:  {  H1(f) where f is Element of PF : S1[f]  }  is finite from PRE_CIRC:sch_1();
 (PFuncs (V,C)) /\  {  (union  {  ((f . i) \ i) where i is Element of PFuncs (V,C) : i in A  }  ) where f is Element of PFuncs (A,B) : dom f = A  }  c= PFuncs (V,C) by XBOOLE_1:17;
hence  (PFuncs (V,C)) /\  {  (union  {  ((f . i) \ i) where i is Element of PFuncs (V,C) : i in A  }  ) where f is Element of PFuncs (A,B) : dom f = A  }  is Element of Fin (PFuncs (V,C)) by A1, A2, FINSUB_1:def_5; ::_thesis: verum
end;
end;

:: deftheorem  defines =>> HEYTING2:def_3_:_
 for V being set
for C being finite set
for A, B being Element of Fin (PFuncs (V,C)) holds A =>> B = (PFuncs (V,C)) /\  {  (union  {  ((f . i) \ i) where i is Element of PFuncs (V,C) : i in A  }  ) where f is Element of PFuncs (A,B) : dom f = A  }  ;

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

Lm3:  for a, V being set
for C being finite set
for A being Element of Fin (PFuncs (V,C))
for K being Element of SubstitutionSet (V,C) st a in A ^ (A =>> K) holds
ex b being set st
( b in K & b c= a )
proof
let a, V be set ; ::_thesis: for C being finite set
for A being Element of Fin (PFuncs (V,C))
for K being Element of SubstitutionSet (V,C) st a in A ^ (A =>> K) holds
ex b being set st
( b in K & b c= a )
let C be finite set ; ::_thesis: for A being Element of Fin (PFuncs (V,C))
for K being Element of SubstitutionSet (V,C) st a in A ^ (A =>> K) holds
ex b being set st
( b in K & b c= a )
let A be Element of Fin (PFuncs (V,C)); ::_thesis: for K being Element of SubstitutionSet (V,C) st a in A ^ (A =>> K) holds
ex b being set st
( b in K & b c= a )
let K be Element of SubstitutionSet (V,C); ::_thesis: ( a in A ^ (A =>> K) implies ex b being set st
( b in K & b c= a ) )
A1: K c= PFuncs (V,C) by FINSUB_1:def_5;
assume  a in A ^ (A =>> K) ; ::_thesis: ex b being set st
( b in K & b c= a )
then consider b, c being set  such that
A2: b in A and
A3: c in A =>> K and
A4: a = b \/ c by SUBSTLAT:15;
 A c= PFuncs (V,C) by FINSUB_1:def_5;
then reconsider b9 = b as Element of PFuncs (V,C) by A2;
consider f being PartFunc of A,K such that
A5: c = union  {  ((f . i) \ i) where i is Element of PFuncs (V,C) : i in A  }  and
A6: dom f = A by A3, Th15;
 f . b in K by A2, A6, PARTFUN1:4;
then reconsider d = f . b as Element of PFuncs (V,C) by A1;
take  d ; ::_thesis: ( d in K & d c= a )
thus  d in K by A2, A6, PARTFUN1:4; ::_thesis: d c= a
 d \ b9 in  {  ((f . i) \ i) where i is Element of PFuncs (V,C) : i in A  }  by A2;
hence  d c= a by A4, A5, XBOOLE_1:44, ZFMISC_1:74; ::_thesis: verum
end;

theorem :: HEYTING2:16
for V being set
for C being finite set
for A being Element of Fin (PFuncs (V,C)) st A = {} holds
A =>> A = {{}}
proof
deffunc H1( set ) ->  set = {} ;
let V be set ; ::_thesis: for C being finite set
for A being Element of Fin (PFuncs (V,C)) st A = {} holds
A =>> A = {{}}
let C be finite set ; ::_thesis: for A being Element of Fin (PFuncs (V,C)) st A = {} holds
A =>> A = {{}}
let A be Element of Fin (PFuncs (V,C)); ::_thesis: ( A = {} implies A =>> A = {{}} )
defpred S1[ Function] means  dom $1 = A;
deffunc H2( Element of PFuncs (A,A)) ->  set = union  {  (($1 . i) \ i) where i is Element of PFuncs (V,C) : i in A  }  ;
A1: ex a being Element of PFuncs (A,A) st S1[a]
proof
reconsider e = id A as Element of PFuncs (A,A) by PARTFUN1:45;
take  e ; ::_thesis: S1[e]
thus  S1[e] by RELAT_1:45; ::_thesis: verum
end;
A2:  {  {} where f is Element of PFuncs (A,A) : S1[f]  }  = {{}} from LATTICE3:sch_1(A1);
assume A3: A = {} ; ::_thesis: A =>> A = {{}}
now__::_thesis:_for_f_being_Element_of_PFuncs_(A,A)_holds__{__((f_._i)_\_i)_where_i_is_Element_of_PFuncs_(V,C)_:_i_in_A__}__=_{}
let f be Element of PFuncs (A,A); ::_thesis:  {  ((f . i) \ i) where i is Element of PFuncs (V,C) : i in A  }  = {}
 for x being set holds not x in  {  ((f . i) \ i) where i is Element of PFuncs (V,C) : i in A  }
proof
given x being set  such that A4: x in  {  ((f . i) \ i) where i is Element of PFuncs (V,C) : i in A  }  ; ::_thesis: contradiction
 ex x1 being Element of PFuncs (V,C) st
( x = (f . x1) \ x1 & x1 in A ) by A4;
hence  contradiction by A3; ::_thesis: verum
end;
hence   {  ((f . i) \ i) where i is Element of PFuncs (V,C) : i in A  }  = {} by XBOOLE_0:def_1; ::_thesis: verum
end;
then A5: for v being Element of PFuncs (A,A) st S1[v] holds
H2(v) = H1(v) by ZFMISC_1:2;
A6:  {  H2(f) where f is Element of PFuncs (A,A) : S1[f]  }  =  {  H1(f) where f is Element of PFuncs (A,A) : S1[f]  }  from FRAENKEL:sch_6(A5);
 {} is PartFunc of V,C by RELSET_1:12;
then  {} in PFuncs (V,C) by PARTFUN1:45;
then  {{}} c= PFuncs (V,C) by ZFMISC_1:31;
hence  A =>> A = {{}} by A6, A2, XBOOLE_1:28; ::_thesis: verum
end;

        Lm4:  for V being set
for C being finite set
for K being Element of SubstitutionSet (V,C)
for X being set st X c= K holds
X in SubstitutionSet (V,C)
proof
let V be set ; ::_thesis: for C being finite set
for K being Element of SubstitutionSet (V,C)
for X being set st X c= K holds
X in SubstitutionSet (V,C)
let C be finite set ; ::_thesis: for K being Element of SubstitutionSet (V,C)
for X being set st X c= K holds
X in SubstitutionSet (V,C)
let K be Element of SubstitutionSet (V,C); ::_thesis: for X being set st X c= K holds
X in SubstitutionSet (V,C)
let X be set ; ::_thesis: ( X c= K implies X in SubstitutionSet (V,C) )
assume A1: X c= K ; ::_thesis: X in SubstitutionSet (V,C)
 K c= PFuncs (V,C) by FINSUB_1:def_5;
then  X c= PFuncs (V,C) by A1, XBOOLE_1:1;
then reconsider B = X as Element of Fin (PFuncs (V,C)) by A1, FINSUB_1:def_5;
A2: for a, b being Element of PFuncs (V,C) st a in B & b in B & a c= b holds
a = b by A1, SUBSTLAT:5;
 for x being set st x in X holds
x is finite by A1, Th1;
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 A2;
hence  X in SubstitutionSet (V,C) by SUBSTLAT:def_1; ::_thesis: verum
end;

theorem Th17: :: HEYTING2:17
for V being set
for C being finite set
for u being Element of (SubstLatt (V,C))
for X being set st X c= u holds
X is Element of (SubstLatt (V,C))
proof
let V be set ; ::_thesis: for C being finite set
for u being Element of (SubstLatt (V,C))
for X being set st X c= u holds
X is Element of (SubstLatt (V,C))
let C be finite set ; ::_thesis: for u being Element of (SubstLatt (V,C))
for X being set st X c= u holds
X is Element of (SubstLatt (V,C))
let u be Element of (SubstLatt (V,C)); ::_thesis: for X being set st X c= u holds
X is Element of (SubstLatt (V,C))
let X be set ; ::_thesis: ( X c= u implies X is Element of (SubstLatt (V,C)) )
reconsider u9 = u as Element of SubstitutionSet (V,C) by SUBSTLAT:def_4;
assume  X c= u ; ::_thesis: X is Element of (SubstLatt (V,C))
then  X c= u9 ;
then  X in SubstitutionSet (V,C) by Lm4;
hence  X is Element of (SubstLatt (V,C)) by SUBSTLAT:def_4; ::_thesis: verum
end;

begin

definition
let V be set ;
let C be finite set ;
func pseudo_compl (V,C) ->  UnOp of the carrier of (SubstLatt (V,C)) means :Def4: :: HEYTING2:def 4
 for u being Element of (SubstLatt (V,C))
for u9 being Element of SubstitutionSet (V,C) st u9 = u holds
it . u = mi (- u9);
existence
 ex b1 being UnOp of the carrier of (SubstLatt (V,C)) st
for u being Element of (SubstLatt (V,C))
for u9 being Element of SubstitutionSet (V,C) st u9 = u holds
b1 . u = mi (- u9)
proof
deffunc H1( Element of SubstitutionSet (V,C)) ->  Element of SubstitutionSet (V,C) = mi (- $1);
consider IT being Function of (SubstitutionSet (V,C)),(SubstitutionSet (V,C)) such that
A1: for u being Element of SubstitutionSet (V,C) holds IT . u = H1(u) from FUNCT_2:sch_4();
 SubstitutionSet (V,C) = the carrier of (SubstLatt (V,C)) by SUBSTLAT:def_4;
then reconsider IT = IT as UnOp of the carrier of (SubstLatt (V,C)) ;
take  IT ; ::_thesis: for u being Element of (SubstLatt (V,C))
for u9 being Element of SubstitutionSet (V,C) st u9 = u holds
IT . u = mi (- u9)
thus  for u being Element of (SubstLatt (V,C))
for u9 being Element of SubstitutionSet (V,C) st u9 = u holds
IT . u = mi (- u9) by A1; ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being UnOp of the carrier of (SubstLatt (V,C)) st ( for u being Element of (SubstLatt (V,C))
for u9 being Element of SubstitutionSet (V,C) st u9 = u holds
b1 . u = mi (- u9) ) & ( for u being Element of (SubstLatt (V,C))
for u9 being Element of SubstitutionSet (V,C) st u9 = u holds
b2 . u = mi (- u9) ) holds
b1 = b2;
proof
let IT, IT9 be UnOp of the carrier of (SubstLatt (V,C)); ::_thesis: ( ( for u being Element of (SubstLatt (V,C))
for u9 being Element of SubstitutionSet (V,C) st u9 = u holds
IT . u = mi (- u9) ) & ( for u being Element of (SubstLatt (V,C))
for u9 being Element of SubstitutionSet (V,C) st u9 = u holds
IT9 . u = mi (- u9) ) implies IT = IT9 )
assume that
A2: for u being Element of (SubstLatt (V,C))
for u9 being Element of SubstitutionSet (V,C) st u9 = u holds
IT . u = mi (- u9) and
A3: for u being Element of (SubstLatt (V,C))
for u9 being Element of SubstitutionSet (V,C) st u9 = u holds
IT9 . u = mi (- u9) ; ::_thesis: IT = IT9
now__::_thesis:_for_u_being_Element_of_(SubstLatt_(V,C))_holds_IT_._u_=_IT9_._u
let u be Element of (SubstLatt (V,C)); ::_thesis: IT . u = IT9 . u
reconsider u9 = u as Element of SubstitutionSet (V,C) by SUBSTLAT:def_4;
thus IT . u = mi (- u9) by A2
.= IT9 . u by A3 ; ::_thesis: verum
end;
hence  IT = IT9 by FUNCT_2:63; ::_thesis: verum
end;
func StrongImpl (V,C) ->  BinOp of the carrier of (SubstLatt (V,C)) means :Def5: :: HEYTING2:def 5
 for u, v being Element of (SubstLatt (V,C))
for u9, v9 being Element of SubstitutionSet (V,C) st u9 = u & v9 = v holds
it . (u,v) = mi (u9 =>> v9);
existence
 ex b1 being BinOp of the carrier of (SubstLatt (V,C)) st
for u, v being Element of (SubstLatt (V,C))
for u9, v9 being Element of SubstitutionSet (V,C) st u9 = u & v9 = v holds
b1 . (u,v) = mi (u9 =>> v9)
proof
set ZA = the carrier of (SubstLatt (V,C));
defpred S1[ set , set , set ] means  for u9, v9 being Element of SubstitutionSet (V,C) st u9 = $1 & v9 = $2 holds
$3 = mi (u9 =>> v9);
A4: for x, y being Element of the carrier of (SubstLatt (V,C)) ex z being Element of the carrier of (SubstLatt (V,C)) st S1[x,y,z]
proof
let x, y be Element of the carrier of (SubstLatt (V,C)); ::_thesis: ex z being Element of the carrier of (SubstLatt (V,C)) st S1[x,y,z]
reconsider x9 = x, y9 = y as Element of SubstitutionSet (V,C) by SUBSTLAT:def_4;
reconsider z = mi (x9 =>> y9) as Element of the carrier of (SubstLatt (V,C)) by SUBSTLAT:def_4;
take  z ; ::_thesis: S1[x,y,z]
let u9, v9 be Element of SubstitutionSet (V,C); ::_thesis: ( u9 = x & v9 = y implies z = mi (u9 =>> v9) )
assume that
A5: u9 = x and
A6: v9 = y ; ::_thesis: z = mi (u9 =>> v9)
thus  z = mi (u9 =>> v9) by A5, A6; ::_thesis: verum
end;
consider o being BinOp of the carrier of (SubstLatt (V,C)) such that
A7: for a, b being Element of (SubstLatt (V,C)) holds S1[a,b,o . (a,b)] from BINOP_1:sch_3(A4);
take  o ; ::_thesis: for u, v being Element of (SubstLatt (V,C))
for u9, v9 being Element of SubstitutionSet (V,C) st u9 = u & v9 = v holds
o . (u,v) = mi (u9 =>> v9)
let u, v be Element of (SubstLatt (V,C)); ::_thesis: for u9, v9 being Element of SubstitutionSet (V,C) st u9 = u & v9 = v holds
o . (u,v) = mi (u9 =>> v9)
let u9, v9 be Element of SubstitutionSet (V,C); ::_thesis: ( u9 = u & v9 = v implies o . (u,v) = mi (u9 =>> v9) )
assume that
A8: u9 = u and
A9: v9 = v ; ::_thesis: o . (u,v) = mi (u9 =>> v9)
thus  o . (u,v) = mi (u9 =>> v9) by A7, A8, A9; ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being BinOp of the carrier of (SubstLatt (V,C)) st ( for u, v being Element of (SubstLatt (V,C))
for u9, v9 being Element of SubstitutionSet (V,C) st u9 = u & v9 = v holds
b1 . (u,v) = mi (u9 =>> v9) ) & ( for u, v being Element of (SubstLatt (V,C))
for u9, v9 being Element of SubstitutionSet (V,C) st u9 = u & v9 = v holds
b2 . (u,v) = mi (u9 =>> v9) ) holds
b1 = b2;
proof
let IT1, IT2 be BinOp of the carrier of (SubstLatt (V,C)); ::_thesis: ( ( for u, v being Element of (SubstLatt (V,C))
for u9, v9 being Element of SubstitutionSet (V,C) st u9 = u & v9 = v holds
IT1 . (u,v) = mi (u9 =>> v9) ) & ( for u, v being Element of (SubstLatt (V,C))
for u9, v9 being Element of SubstitutionSet (V,C) st u9 = u & v9 = v holds
IT2 . (u,v) = mi (u9 =>> v9) ) implies IT1 = IT2 )
assume that
A10: for u, v being Element of (SubstLatt (V,C))
for u9, v9 being Element of SubstitutionSet (V,C) st u9 = u & v9 = v holds
IT1 . (u,v) = mi (u9 =>> v9) and
A11: for u, v being Element of (SubstLatt (V,C))
for u9, v9 being Element of SubstitutionSet (V,C) st u9 = u & v9 = v holds
IT2 . (u,v) = mi (u9 =>> v9) ; ::_thesis: IT1 = IT2
now__::_thesis:_for_u,_v_being_Element_of_(SubstLatt_(V,C))_holds_IT1_._(u,v)_=_IT2_._(u,v)
let u, v be Element of (SubstLatt (V,C)); ::_thesis: IT1 . (u,v) = IT2 . (u,v)
reconsider u9 = u, v9 = v as Element of SubstitutionSet (V,C) by SUBSTLAT:def_4;
thus IT1 . (u,v) = mi (u9 =>> v9) by A10
.= IT2 . (u,v) by A11 ; ::_thesis: verum
end;
hence  IT1 = IT2 by BINOP_1:2; ::_thesis: verum
end;
let u be Element of (SubstLatt (V,C));
func SUB u ->  Element of Fin the carrier of (SubstLatt (V,C)) equals :: HEYTING2:def 6
 bool u;
coherence
 bool u is Element of Fin the carrier of (SubstLatt (V,C))
proof
reconsider u9 = u as Element of SubstitutionSet (V,C) by SUBSTLAT:def_4;
A12: bool u c= the carrier of (SubstLatt (V,C))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in bool u or x in the carrier of (SubstLatt (V,C)) )
assume  x in bool u ; ::_thesis: x in the carrier of (SubstLatt (V,C))
then  x is Element of (SubstLatt (V,C)) by Th17;
hence  x in the carrier of (SubstLatt (V,C)) ; ::_thesis: verum
end;
 u9 is finite ;
hence  bool u is Element of Fin the carrier of (SubstLatt (V,C)) by A12, FINSUB_1:def_5; ::_thesis: verum
end;
correctness
;
func diff u ->  UnOp of the carrier of (SubstLatt (V,C)) means :Def7: :: HEYTING2:def 7
 for v being Element of (SubstLatt (V,C)) holds it . v = u \ v;
existence
 ex b1 being UnOp of the carrier of (SubstLatt (V,C)) st
for v being Element of (SubstLatt (V,C)) holds b1 . v = u \ v
proof
deffunc H1( set ) ->  Element of bool u = u \ $1;
consider IT being Function such that
A13: ( dom IT = the carrier of (SubstLatt (V,C)) & ( for v being set st v in the carrier of (SubstLatt (V,C)) holds
IT . v = H1(v) ) ) from FUNCT_1:sch_3();
 u in the carrier of (SubstLatt (V,C)) ;
then A14: u in SubstitutionSet (V,C) by SUBSTLAT:def_4;
 for x being set st x in the carrier of (SubstLatt (V,C)) holds
IT . x in Fin (PFuncs (V,C))
proof
let x be set ; ::_thesis: ( x in the carrier of (SubstLatt (V,C)) implies IT . x in Fin (PFuncs (V,C)) )
assume  x in the carrier of (SubstLatt (V,C)) ; ::_thesis: IT . x in Fin (PFuncs (V,C))
then A15: IT . x = u \ x by A13;
 u \ x in SubstitutionSet (V,C) by A14, Lm4;
hence  IT . x in Fin (PFuncs (V,C)) by A15; ::_thesis: verum
end;
then reconsider IT = IT as Function of the carrier of (SubstLatt (V,C)),(Fin (PFuncs (V,C))) by A13, FUNCT_2:3;
now__::_thesis:_for_v_being_Element_of_(SubstLatt_(V,C))_holds_IT_._v_in_the_carrier_of_(SubstLatt_(V,C))
let v be Element of (SubstLatt (V,C)); ::_thesis: IT . v in the carrier of (SubstLatt (V,C))
 u \ v in SubstitutionSet (V,C) by A14, Lm4;
then  IT . v in SubstitutionSet (V,C) by A13;
hence  IT . v in the carrier of (SubstLatt (V,C)) by SUBSTLAT:def_4; ::_thesis: verum
end;
then reconsider IT = IT as UnOp of the carrier of (SubstLatt (V,C)) by HEYTING1:1;
take  IT ; ::_thesis: for v being Element of (SubstLatt (V,C)) holds IT . v = u \ v
let v be Element of (SubstLatt (V,C)); ::_thesis: IT . v = u \ v
thus  IT . v = u \ v by A13; ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being UnOp of the carrier of (SubstLatt (V,C)) st ( for v being Element of (SubstLatt (V,C)) holds b1 . v = u \ v ) & ( for v being Element of (SubstLatt (V,C)) holds b2 . v = u \ v ) holds
b1 = b2;
proof
let IT, IT9 be UnOp of the carrier of (SubstLatt (V,C)); ::_thesis: ( ( for v being Element of (SubstLatt (V,C)) holds IT . v = u \ v ) & ( for v being Element of (SubstLatt (V,C)) holds IT9 . v = u \ v ) implies IT = IT9 )
assume that
A16: for v being Element of (SubstLatt (V,C)) holds IT . v = u \ v and
A17: for v being Element of (SubstLatt (V,C)) holds IT9 . v = u \ v ; ::_thesis: IT = IT9
now__::_thesis:_for_v_being_Element_of_(SubstLatt_(V,C))_holds_IT_._v_=_IT9_._v
let v be Element of (SubstLatt (V,C)); ::_thesis: IT . v = IT9 . v
thus IT . v = u \ v by A16
.= IT9 . v by A17 ; ::_thesis: verum
end;
hence  IT = IT9 by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines pseudo_compl HEYTING2:def_4_:_
 for V being set
for C being finite set
for b3 being UnOp of the carrier of (SubstLatt (V,C)) holds
( b3 = pseudo_compl (V,C) iff for u being Element of (SubstLatt (V,C))
for u9 being Element of SubstitutionSet (V,C) st u9 = u holds
b3 . u = mi (- u9) );

:: deftheorem Def5 defines StrongImpl HEYTING2:def_5_:_
 for V being set
for C being finite set
for b3 being BinOp of the carrier of (SubstLatt (V,C)) holds
( b3 = StrongImpl (V,C) iff for u, v being Element of (SubstLatt (V,C))
for u9, v9 being Element of SubstitutionSet (V,C) st u9 = u & v9 = v holds
b3 . (u,v) = mi (u9 =>> v9) );

:: deftheorem  defines SUB HEYTING2:def_6_:_
 for V being set
for C being finite set
for u being Element of (SubstLatt (V,C)) holds SUB u = bool u;

:: deftheorem Def7 defines diff HEYTING2:def_7_:_
 for V being set
for C being finite set
for u being Element of (SubstLatt (V,C))
for b4 being UnOp of the carrier of (SubstLatt (V,C)) holds
( b4 = diff u iff for v being Element of (SubstLatt (V,C)) holds b4 . v = u \ v );

Lm5:  for V being set
for C being finite set
for v, u being Element of (SubstLatt (V,C)) st v in SUB u holds
v "\/" ((diff u) . v) = u
proof
let V be set ; ::_thesis: for C being finite set
for v, u being Element of (SubstLatt (V,C)) st v in SUB u holds
v "\/" ((diff u) . v) = u
let C be finite set ; ::_thesis: for v, u being Element of (SubstLatt (V,C)) st v in SUB u holds
v "\/" ((diff u) . v) = u
let v, u be Element of (SubstLatt (V,C)); ::_thesis: ( v in SUB u implies v "\/" ((diff u) . v) = u )
assume A1: v in SUB u ; ::_thesis: v "\/" ((diff u) . v) = u
reconsider u9 = u, v9 = v, dv = (diff u) . v as Element of SubstitutionSet (V,C) by SUBSTLAT:def_4;
A2: u \ v = (diff u) . v by Def7;
thus v "\/" ((diff u) . v) = the L_join of (SubstLatt (V,C)) . (v,((diff u) . v)) by LATTICES:def_1
.= mi (v9 \/ dv) by SUBSTLAT:def_4
.= mi u9 by A1, A2, XBOOLE_1:45
.= u by SUBSTLAT:11 ; ::_thesis: verum
end;

Lm6:  for V being set
for C being finite set
for u being Element of (SubstLatt (V,C))
for a being Element of PFuncs (V,C)
for K being Element of Fin (PFuncs (V,C)) st K = {a} holds
ex v being Element of SubstitutionSet (V,C) st
( v in SUB u & v ^ K = {} & ( for b being Element of PFuncs (V,C) st b in (diff u) . v holds
b tolerates a ) )
proof
let V be set ; ::_thesis: for C being finite set
for u being Element of (SubstLatt (V,C))
for a being Element of PFuncs (V,C)
for K being Element of Fin (PFuncs (V,C)) st K = {a} holds
ex v being Element of SubstitutionSet (V,C) st
( v in SUB u & v ^ K = {} & ( for b being Element of PFuncs (V,C) st b in (diff u) . v holds
b tolerates a ) )
let C be finite set ; ::_thesis: for u being Element of (SubstLatt (V,C))
for a being Element of PFuncs (V,C)
for K being Element of Fin (PFuncs (V,C)) st K = {a} holds
ex v being Element of SubstitutionSet (V,C) st
( v in SUB u & v ^ K = {} & ( for b being Element of PFuncs (V,C) st b in (diff u) . v holds
b tolerates a ) )
let u be Element of (SubstLatt (V,C)); ::_thesis: for a being Element of PFuncs (V,C)
for K being Element of Fin (PFuncs (V,C)) st K = {a} holds
ex v being Element of SubstitutionSet (V,C) st
( v in SUB u & v ^ K = {} & ( for b being Element of PFuncs (V,C) st b in (diff u) . v holds
b tolerates a ) )
let a be Element of PFuncs (V,C); ::_thesis: for K being Element of Fin (PFuncs (V,C)) st K = {a} holds
ex v being Element of SubstitutionSet (V,C) st
( v in SUB u & v ^ K = {} & ( for b being Element of PFuncs (V,C) st b in (diff u) . v holds
b tolerates a ) )
deffunc H1( set ) ->  set = $1;
let K be Element of Fin (PFuncs (V,C)); ::_thesis: ( K = {a} implies ex v being Element of SubstitutionSet (V,C) st
( v in SUB u & v ^ K = {} & ( for b being Element of PFuncs (V,C) st b in (diff u) . v holds
b tolerates a ) ) )
assume A1: K = {a} ; ::_thesis: ex v being Element of SubstitutionSet (V,C) st
( v in SUB u & v ^ K = {} & ( for b being Element of PFuncs (V,C) st b in (diff u) . v holds
b tolerates a ) )
deffunc H2( Element of PFuncs (V,C), Element of PFuncs (V,C)) ->  set = $1 \/ $2;
defpred S1[ Element of PFuncs (V,C)] means ( not $1 tolerates a & $1 in u & $1 tolerates a );
deffunc H3( Element of PFuncs (V,C), Element of PFuncs (V,C)) ->  set = $1 \/ $2;
defpred S2[ Element of PFuncs (V,C)] means ( $1 is finite & not $1 tolerates a );
set M =  {  H1(s) where s is Element of PFuncs (V,C) : ( H1(s) in u & S2[s] )  }  ;
defpred S3[ Element of PFuncs (V,C), Element of PFuncs (V,C)] means ( $1 in  {  H1(s) where s is Element of PFuncs (V,C) : ( H1(s) in u & S2[s] )  }  & $2 in {a} & $1 tolerates $2 );
defpred S4[ Element of PFuncs (V,C), Element of PFuncs (V,C)] means ( $2 = a & $1 in  {  H1(s) where s is Element of PFuncs (V,C) : ( H1(s) in u & S2[s] )  }  & $1 tolerates $2 );
defpred S5[ Element of PFuncs (V,C)] means ( $1 in  {  H1(s) where s is Element of PFuncs (V,C) : ( H1(s) in u & S2[s] )  }  & $1 tolerates a );
defpred S6[ Element of PFuncs (V,C), Element of PFuncs (V,C)] means ( $1 in  {  H1(s) where s is Element of PFuncs (V,C) : ( H1(s) in u & S2[s] )  }  & $1 tolerates $2 );
deffunc H4( Element of PFuncs (V,C)) ->  set = $1 \/ a;
A2:  {  H1(s) where s is Element of PFuncs (V,C) : ( H1(s) in u & S2[s] )  }  c= u from FRAENKEL:sch_17();
then reconsider v =  {  H1(s) where s is Element of PFuncs (V,C) : ( H1(s) in u & S2[s] )  }  as Element of (SubstLatt (V,C)) by Th17;
reconsider v = v as Element of SubstitutionSet (V,C) by SUBSTLAT:def_4;
take  v ; ::_thesis: ( v in SUB u & v ^ K = {} & ( for b being Element of PFuncs (V,C) st b in (diff u) . v holds
b tolerates a ) )
thus  v in SUB u by A2; ::_thesis: ( v ^ K = {} & ( for b being Element of PFuncs (V,C) st b in (diff u) . v holds
b tolerates a ) )
A3: for s, t being Element of PFuncs (V,C) holds
( S3[s,t] iff S4[s,t] ) by TARSKI:def_1;
A4:  {  H3(s,t) where s, t is Element of PFuncs (V,C) : S3[s,t]  }  =  {  H3(s9,t9) where s9, t9 is Element of PFuncs (V,C) : S4[s9,t9]  }  from FRAENKEL:sch_4(A3);
 for s being Element of PFuncs (V,C) holds
( s in  {  H1(s) where s is Element of PFuncs (V,C) : ( H1(s) in u & S2[s] )  }  iff ( s is finite & not s tolerates a & s in u ) )
proof
let s be Element of PFuncs (V,C); ::_thesis: ( s in  {  H1(s) where s is Element of PFuncs (V,C) : ( H1(s) in u & S2[s] )  }  iff ( s is finite & not s tolerates a & s in u ) )
thus  ( s in  {  H1(s) where s is Element of PFuncs (V,C) : ( H1(s) in u & S2[s] )  }  implies ( s is finite & not s tolerates a & s in u ) ) ::_thesis: ( s is finite & not s tolerates a & s in u implies s in  {  H1(s) where s is Element of PFuncs (V,C) : ( H1(s) in u & S2[s] )  }  )
proof
assume  s in  {  H1(s) where s is Element of PFuncs (V,C) : ( H1(s) in u & S2[s] )  }  ; ::_thesis: ( s is finite & not s tolerates a & s in u )
then  ex s2 being Element of PFuncs (V,C) st
( s2 = s & s2 in u & s2 is finite & not s2 tolerates a ) ;
hence  ( s is finite & not s tolerates a & s in u ) ; ::_thesis: verum
end;
thus  ( s is finite & not s tolerates a & s in u implies s in  {  H1(s) where s is Element of PFuncs (V,C) : ( H1(s) in u & S2[s] )  }  ) ; ::_thesis: verum
end;
then A5: for s being Element of PFuncs (V,C) holds
( S5[s] iff S1[s] ) ;
A6:  {  H4(s9) where s9 is Element of PFuncs (V,C) : S5[s9]  }  =  {  H4(s) where s is Element of PFuncs (V,C) : S1[s]  }  from FRAENKEL:sch_3(A5);
  {  H2(s,t) where s, t is Element of PFuncs (V,C) : ( t = a & S6[s,t] )  }  =  {  H2(s9,a) where s9 is Element of PFuncs (V,C) : S6[s9,a]  }  from FRAENKEL:sch_20();
then A7: v ^ K =  {  (s \/ a) where s is Element of PFuncs (V,C) : ( not s tolerates a & s in u & s tolerates a )  }  by A1, A4, A6, SUBSTLAT:def_3;
thus  v ^ K = {} ::_thesis: for b being Element of PFuncs (V,C) st b in (diff u) . v holds
b tolerates a
proof
assume  v ^ K <> {} ; ::_thesis: contradiction
then consider x being set  such that
A8: x in v ^ K by XBOOLE_0:def_1;
 ex s1 being Element of PFuncs (V,C) st
( x = s1 \/ a & not s1 tolerates a & s1 in u & s1 tolerates a ) by A7, A8;
hence  contradiction ; ::_thesis: verum
end;
let b be Element of PFuncs (V,C); ::_thesis: ( b in (diff u) . v implies b tolerates a )
assume  b in (diff u) . v ; ::_thesis: b tolerates a
then A9: b in u \ v by Def7;
then A10: not b in  {  H1(s) where s is Element of PFuncs (V,C) : ( H1(s) in u & S2[s] )  }  by XBOOLE_0:def_5;
 u in the carrier of (SubstLatt (V,C)) ;
then  u in SubstitutionSet (V,C) by SUBSTLAT:def_4;
then  b is finite by A9, Th1;
hence  b tolerates a by A9, A10; ::_thesis: verum
end;

definition
let V be set ;
let C be finite set ;
func Atom (V,C) ->  Function of (PFuncs (V,C)), the carrier of (SubstLatt (V,C)) means :Def8: :: HEYTING2:def 8
 for a being Element of PFuncs (V,C) holds it . a = mi {.a.};
existence
 ex b1 being Function of (PFuncs (V,C)), the carrier of (SubstLatt (V,C)) st
for a being Element of PFuncs (V,C) holds b1 . a = mi {.a.}
proof
deffunc H1( Element of PFuncs (V,C)) ->  Element of SubstitutionSet (V,C) = mi {.$1.};
consider f being Function of (PFuncs (V,C)),(SubstitutionSet (V,C)) such that
A1: for a being Element of PFuncs (V,C) holds f . a = H1(a) from FUNCT_2:sch_4();
A2: the carrier of (SubstLatt (V,C)) = SubstitutionSet (V,C) by SUBSTLAT:def_4;
A3: now__::_thesis:_for_x_being_set_st_x_in_PFuncs_(V,C)_holds_
f_._x_in_the_carrier_of_(SubstLatt_(V,C))
let x be set ; ::_thesis: ( x in PFuncs (V,C) implies f . x in the carrier of (SubstLatt (V,C)) )
assume  x in PFuncs (V,C) ; ::_thesis: f . x in the carrier of (SubstLatt (V,C))
then reconsider a = x as Element of PFuncs (V,C) ;
 f . a = mi {.a.} by A1;
hence  f . x in the carrier of (SubstLatt (V,C)) by A2; ::_thesis: verum
end;
 dom f = PFuncs (V,C) by FUNCT_2:def_1;
then reconsider f = f as Function of (PFuncs (V,C)), the carrier of (SubstLatt (V,C)) by A3, FUNCT_2:3;
take  f ; ::_thesis: for a being Element of PFuncs (V,C) holds f . a = mi {.a.}
thus  for a being Element of PFuncs (V,C) holds f . a = mi {.a.} by A1; ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being Function of (PFuncs (V,C)), the carrier of (SubstLatt (V,C)) st ( for a being Element of PFuncs (V,C) holds b1 . a = mi {.a.} ) & ( for a being Element of PFuncs (V,C) holds b2 . a = mi {.a.} ) holds
b1 = b2;
proof
let IT1, IT2 be Function of (PFuncs (V,C)), the carrier of (SubstLatt (V,C)); ::_thesis: ( ( for a being Element of PFuncs (V,C) holds IT1 . a = mi {.a.} ) & ( for a being Element of PFuncs (V,C) holds IT2 . a = mi {.a.} ) implies IT1 = IT2 )
assume that
A4: for a being Element of PFuncs (V,C) holds IT1 . a = mi {.a.} and
A5: for a being Element of PFuncs (V,C) holds IT2 . a = mi {.a.} ; ::_thesis: IT1 = IT2
now__::_thesis:_for_a_being_Element_of_PFuncs_(V,C)_holds_IT1_._a_=_IT2_._a
let a be Element of PFuncs (V,C); ::_thesis: IT1 . a = IT2 . a
 IT1 . a = mi {.a.} by A4;
hence  IT1 . a = IT2 . a by A5; ::_thesis: verum
end;
hence  IT1 = IT2 by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def8 defines Atom HEYTING2:def_8_:_
 for V being set
for C being finite set
for b3 being Function of (PFuncs (V,C)), the carrier of (SubstLatt (V,C)) holds
( b3 = Atom (V,C) iff for a being Element of PFuncs (V,C) holds b3 . a = mi {.a.} );

Lm7:  for V being set
for C being finite set
for a being Element of PFuncs (V,C) st a is finite holds
(Atom (V,C)) . a = {a}
proof
let V be set ; ::_thesis: for C being finite set
for a being Element of PFuncs (V,C) st a is finite holds
(Atom (V,C)) . a = {a}
let C be finite set ; ::_thesis: for a being Element of PFuncs (V,C) st a is finite holds
(Atom (V,C)) . a = {a}
let a be Element of PFuncs (V,C); ::_thesis: ( a is finite implies (Atom (V,C)) . a = {a} )
A1: for s, t being Element of PFuncs (V,C) st s in {a} & t in {a} & s c= t holds
s = t
proof
let s, t be Element of PFuncs (V,C); ::_thesis: ( s in {a} & t in {a} & s c= t implies s = t )
assume that
A2: s in {a} and
A3: t in {a} and
 s c= t ; ::_thesis: s = t
 s = a by A2, TARSKI:def_1;
hence  s = t by A3, TARSKI:def_1; ::_thesis: verum
end;
assume  a is finite ; ::_thesis: (Atom (V,C)) . a = {a}
then  for u being set st u in {a} holds
u is finite ;
then  {.a.} 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 A1;
then  {a} in SubstitutionSet (V,C) by SUBSTLAT:def_1;
then {a} = mi {.a.} by SUBSTLAT:11
.= (Atom (V,C)) . a by Def8 ;
hence  (Atom (V,C)) . a = {a} ; ::_thesis: verum
end;

theorem Th18: :: HEYTING2:18
for V being set
for C being finite set
for K being Element of SubstitutionSet (V,C) holds FinJoin (K,(Atom (V,C))) = FinUnion (K,(singleton (PFuncs (V,C))))
proof
let V be set ; ::_thesis: for C being finite set
for K being Element of SubstitutionSet (V,C) holds FinJoin (K,(Atom (V,C))) = FinUnion (K,(singleton (PFuncs (V,C))))
let C be finite set ; ::_thesis: for K being Element of SubstitutionSet (V,C) holds FinJoin (K,(Atom (V,C))) = FinUnion (K,(singleton (PFuncs (V,C))))
let K be Element of SubstitutionSet (V,C); ::_thesis: FinJoin (K,(Atom (V,C))) = FinUnion (K,(singleton (PFuncs (V,C))))
deffunc H1( Element of Fin (PFuncs (V,C))) ->  Element of SubstitutionSet (V,C) = mi $1;
A1: FinUnion (K,(singleton (PFuncs (V,C)))) c= mi (FinUnion (K,(singleton (PFuncs (V,C)))))
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in FinUnion (K,(singleton (PFuncs (V,C)))) or a in mi (FinUnion (K,(singleton (PFuncs (V,C))))) )
assume A2: a in FinUnion (K,(singleton (PFuncs (V,C)))) ; ::_thesis: a in mi (FinUnion (K,(singleton (PFuncs (V,C)))))
then consider b being Element of PFuncs (V,C) such that
A3: b in K and
A4: a in (singleton (PFuncs (V,C))) . b by SETWISEO:57;
A5: a = b by A4, SETWISEO:55;
A6: now__::_thesis:_for_s_being_finite_set_st_s_in_FinUnion_(K,(singleton_(PFuncs_(V,C))))_&_s_c=_a_holds_
s_=_a
 K in SubstitutionSet (V,C) ;
then  K 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 A7: ex AA being Element of Fin (PFuncs (V,C)) st
( K = AA & ( for u being set st u in AA holds
u is finite ) & ( for s, t being Element of PFuncs (V,C) st s in AA & t in AA & s c= t holds
s = t ) ) ;
let s be finite set ; ::_thesis: ( s in FinUnion (K,(singleton (PFuncs (V,C)))) & s c= a implies s = a )
assume that
A8: s in FinUnion (K,(singleton (PFuncs (V,C)))) and
A9: s c= a ; ::_thesis: s = a
consider t being Element of PFuncs (V,C) such that
A10: t in K and
A11: s in (singleton (PFuncs (V,C))) . t by A8, SETWISEO:57;
 s = t by A11, SETWISEO:55;
hence  s = a by A3, A5, A9, A10, A7; ::_thesis: verum
end;
 a is finite by A3, A5, Th1;
hence  a in mi (FinUnion (K,(singleton (PFuncs (V,C))))) by A2, A6, SUBSTLAT:7; ::_thesis: verum
end;
consider g being Function of (Fin (PFuncs (V,C))),(SubstitutionSet (V,C)) such that
A12: for B being Element of Fin (PFuncs (V,C)) holds g . B = H1(B) from FUNCT_2:sch_4();
reconsider g = g as Function of (Fin (PFuncs (V,C))), the carrier of (SubstLatt (V,C)) by SUBSTLAT:def_4;
A13: now__::_thesis:_for_x,_y_being_Element_of_Fin_(PFuncs_(V,C))_holds_g_._(x_\/_y)_=_the_L_join_of_(SubstLatt_(V,C))_._((g_._x),(g_._y))
let x, y be Element of Fin (PFuncs (V,C)); ::_thesis: g . (x \/ y) = the L_join of (SubstLatt (V,C)) . ((g . x),(g . y))
A14: g . x = mi x by A12;
A15: g . y = mi y by A12;
thus g . (x \/ y) = mi (x \/ y) by A12
.= mi ((mi x) \/ y) by SUBSTLAT:13
.= mi ((mi x) \/ (mi y)) by SUBSTLAT:13
.= the L_join of (SubstLatt (V,C)) . ((g . x),(g . y)) by A14, A15, SUBSTLAT:def_4 ; ::_thesis: verum
end;
A16: now__::_thesis:_for_a_being_set_st_a_in_K_holds_
((g_*_(singleton_(PFuncs_(V,C))))_|_K)_._a_=_((Atom_(V,C))_|_K)_._a
let a be set ; ::_thesis: ( a in K implies ((g * (singleton (PFuncs (V,C)))) | K) . a = ((Atom (V,C)) | K) . a )
assume A17: a in K ; ::_thesis: ((g * (singleton (PFuncs (V,C)))) | K) . a = ((Atom (V,C)) | K) . a
then reconsider a9 = a as Element of PFuncs (V,C) by SETWISEO:9;
A18: a9 is finite by A17, Th1;
then reconsider KL = {a9} as Element of SubstitutionSet (V,C) by Th2;
thus ((g * (singleton (PFuncs (V,C)))) | K) . a = (g * (singleton (PFuncs (V,C)))) . a by A17, FUNCT_1:49
.= g . ((singleton (PFuncs (V,C))) . a9) by FUNCT_2:15
.= g . {a} by SETWISEO:54
.= mi KL by A12
.= KL by SUBSTLAT:11
.= (Atom (V,C)) . a9 by A18, Lm7
.= ((Atom (V,C)) | K) . a by A17, FUNCT_1:49 ; ::_thesis: verum
end;
A19: mi (FinUnion (K,(singleton (PFuncs (V,C))))) c= FinUnion (K,(singleton (PFuncs (V,C)))) by SUBSTLAT:8;
A20: rng (singleton (PFuncs (V,C))) c= Fin (PFuncs (V,C)) ;
A21: K c= PFuncs (V,C) by FINSUB_1:def_5;
then  K c= dom (Atom (V,C)) by FUNCT_2:def_1;
then A22: dom ((Atom (V,C)) | K) = K by RELAT_1:62;
reconsider gs = g * (singleton (PFuncs (V,C))) as Function of (PFuncs (V,C)), the carrier of (SubstLatt (V,C)) ;
A23: g . ({}. (PFuncs (V,C))) = mi ({}. (PFuncs (V,C))) by A12
.= {} by SUBSTLAT:9
.= Bottom (SubstLatt (V,C)) by SUBSTLAT:26
.= the_unity_wrt the L_join of (SubstLatt (V,C)) by LATTICE2:18 ;
 dom g = Fin (PFuncs (V,C)) by FUNCT_2:def_1;
then A24: dom (g * (singleton (PFuncs (V,C)))) = dom (singleton (PFuncs (V,C))) by A20, RELAT_1:27;
 dom (singleton (PFuncs (V,C))) = PFuncs (V,C) by FUNCT_2:def_1;
then  dom ((g * (singleton (PFuncs (V,C)))) | K) = K by A21, A24, RELAT_1:62;
hence  FinJoin (K,(Atom (V,C))) = FinJoin (K,gs) by A22, A16, FUNCT_1:2, LATTICE2:53
.= the L_join of (SubstLatt (V,C)) $$ (K,gs) by LATTICE2:def_3
.= g . (FinUnion (K,(singleton (PFuncs (V,C))))) by A23, A13, SETWISEO:53
.= mi (FinUnion (K,(singleton (PFuncs (V,C))))) by A12
.= FinUnion (K,(singleton (PFuncs (V,C)))) by A19, A1, XBOOLE_0:def_10 ;
::_thesis: verum
end;

theorem Th19: :: HEYTING2:19
for V being set
for C being finite set
for u being Element of SubstitutionSet (V,C) holds u = FinJoin (u,(Atom (V,C)))
proof
let V be set ; ::_thesis: for C being finite set
for u being Element of SubstitutionSet (V,C) holds u = FinJoin (u,(Atom (V,C)))
let C be finite set ; ::_thesis: for u being Element of SubstitutionSet (V,C) holds u = FinJoin (u,(Atom (V,C)))
let u be Element of SubstitutionSet (V,C); ::_thesis: u = FinJoin (u,(Atom (V,C)))
thus u = FinUnion (u,(singleton (PFuncs (V,C)))) by SETWISEO:58
.= FinJoin (u,(Atom (V,C))) by Th18 ; ::_thesis: verum
end;

Lm8:  for V being set
for C being finite set
for u, v being Element of (SubstLatt (V,C)) st ( for a being set st a in u holds
ex b being set st
( b in v & b c= a ) ) holds
u [= v
proof
let V be set ; ::_thesis: for C being finite set
for u, v being Element of (SubstLatt (V,C)) st ( for a being set st a in u holds
ex b being set st
( b in v & b c= a ) ) holds
u [= v
let C be finite set ; ::_thesis: for u, v being Element of (SubstLatt (V,C)) st ( for a being set st a in u holds
ex b being set st
( b in v & b c= a ) ) holds
u [= v
let u, v be Element of (SubstLatt (V,C)); ::_thesis: ( ( for a being set st a in u holds
ex b being set st
( b in v & b c= a ) ) implies u [= v )
assume A1: for a being set st a in u holds
ex b being set st
( b in v & b c= a ) ; ::_thesis: u [= v
reconsider u9 = u, v9 = v as Element of SubstitutionSet (V,C) by SUBSTLAT:def_4;
u "/\" v = the L_meet of (SubstLatt (V,C)) . (u9,v9) by LATTICES:def_2
.= mi (u9 ^ v9) by SUBSTLAT:def_4
.= u9 by A1, Th5 ;
hence  u [= v by LATTICES:4; ::_thesis: verum
end;

theorem Th20: :: HEYTING2:20
for V being set
for C being finite set
for u, v being Element of (SubstLatt (V,C)) holds (diff u) . v [= u
proof
let V be set ; ::_thesis: for C being finite set
for u, v being Element of (SubstLatt (V,C)) holds (diff u) . v [= u
let C be finite set ; ::_thesis: for u, v being Element of (SubstLatt (V,C)) holds (diff u) . v [= u
let u, v be Element of (SubstLatt (V,C)); ::_thesis: (diff u) . v [= u
 (diff u) . v = u \ v by Def7;
then  for a being set st a in (diff u) . v holds
ex b being set st
( b in u & b c= a ) ;
hence  (diff u) . v [= u by Lm8; ::_thesis: verum
end;

theorem Th21: :: HEYTING2:21
for V being set
for C being finite set
for a being Element of PFuncs (V,C) st a is finite holds
for c being set st c in (Atom (V,C)) . a holds
c = a
proof
let V be set ; ::_thesis: for C being finite set
for a being Element of PFuncs (V,C) st a is finite holds
for c being set st c in (Atom (V,C)) . a holds
c = a
let C be finite set ; ::_thesis: for a being Element of PFuncs (V,C) st a is finite holds
for c being set st c in (Atom (V,C)) . a holds
c = a
let a be Element of PFuncs (V,C); ::_thesis: ( a is finite implies for c being set st c in (Atom (V,C)) . a holds
c = a )
assume  a is finite ; ::_thesis: for c being set st c in (Atom (V,C)) . a holds
c = a
then  (Atom (V,C)) . a = {a} by Lm7;
hence  for c being set st c in (Atom (V,C)) . a holds
c = a by TARSKI:def_1; ::_thesis: verum
end;

theorem Th22: :: HEYTING2:22
for V being set
for C being finite set
for u being Element of (SubstLatt (V,C))
for K, L being Element of SubstitutionSet (V,C)
for a being Element of PFuncs (V,C) st K = {a} & L = u & L ^ K = {} holds
(Atom (V,C)) . a [= (pseudo_compl (V,C)) . u
proof
let V be set ; ::_thesis: for C being finite set
for u being Element of (SubstLatt (V,C))
for K, L being Element of SubstitutionSet (V,C)
for a being Element of PFuncs (V,C) st K = {a} & L = u & L ^ K = {} holds
(Atom (V,C)) . a [= (pseudo_compl (V,C)) . u
let C be finite set ; ::_thesis: for u being Element of (SubstLatt (V,C))
for K, L being Element of SubstitutionSet (V,C)
for a being Element of PFuncs (V,C) st K = {a} & L = u & L ^ K = {} holds
(Atom (V,C)) . a [= (pseudo_compl (V,C)) . u
let u be Element of (SubstLatt (V,C)); ::_thesis: for K, L being Element of SubstitutionSet (V,C)
for a being Element of PFuncs (V,C) st K = {a} & L = u & L ^ K = {} holds
(Atom (V,C)) . a [= (pseudo_compl (V,C)) . u
let K, L be Element of SubstitutionSet (V,C); ::_thesis: for a being Element of PFuncs (V,C) st K = {a} & L = u & L ^ K = {} holds
(Atom (V,C)) . a [= (pseudo_compl (V,C)) . u
let a be Element of PFuncs (V,C); ::_thesis: ( K = {a} & L = u & L ^ K = {} implies (Atom (V,C)) . a [= (pseudo_compl (V,C)) . u )
assume that
A1: K = {a} and
A2: L = u and
A3: L ^ K = {} ; ::_thesis: (Atom (V,C)) . a [= (pseudo_compl (V,C)) . u
 a in K by A1, TARSKI:def_1;
then A4: a is finite by Th1;
now__::_thesis:_for_c_being_set_st_c_in_(Atom_(V,C))_._a_holds_
ex_e_being_set_st_
(_e_in_(pseudo_compl_(V,C))_._u_&_e_c=_c_)
let c be set ; ::_thesis: ( c in (Atom (V,C)) . a implies ex e being set st
( e in (pseudo_compl (V,C)) . u & e c= c ) )
assume A5: c in (Atom (V,C)) . a ; ::_thesis: ex e being set st
( e in (pseudo_compl (V,C)) . u & e c= c )
then reconsider c9 = c as Element of PFuncs (V,C) by A4, Th21;
 c = a by A4, A5, Th21;
then consider b being finite set  such that
A6: b in - L and
A7: b c= c9 by A1, A3, Th14;
consider d being set  such that
A8: d c= b and
A9: d in mi (- L) by A6, SUBSTLAT:10;
take e = d; ::_thesis: ( e in (pseudo_compl (V,C)) . u & e c= c )
thus  e in (pseudo_compl (V,C)) . u by A2, A9, Def4; ::_thesis: e c= c
thus  e c= c by A7, A8, XBOOLE_1:1; ::_thesis: verum
end;
hence  (Atom (V,C)) . a [= (pseudo_compl (V,C)) . u by Lm8; ::_thesis: verum
end;

theorem Th23: :: HEYTING2:23
for V being set
for C being finite set
for a being finite Element of PFuncs (V,C) holds a in (Atom (V,C)) . a
proof
let V be set ; ::_thesis: for C being finite set
for a being finite Element of PFuncs (V,C) holds a in (Atom (V,C)) . a
let C be finite set ; ::_thesis: for a being finite Element of PFuncs (V,C) holds a in (Atom (V,C)) . a
let a be finite Element of PFuncs (V,C); ::_thesis: a in (Atom (V,C)) . a
 (Atom (V,C)) . a = {a} by Lm7;
hence  a in (Atom (V,C)) . a by TARSKI:def_1; ::_thesis: verum
end;

Lm9:  for V being set
for C being finite set
for u, v being Element of (SubstLatt (V,C)) st u [= v holds
for x being set st x in u holds
ex b being set st
( b in v & b c= x )
proof
let V be set ; ::_thesis: for C being finite set
for u, v being Element of (SubstLatt (V,C)) st u [= v holds
for x being set st x in u holds
ex b being set st
( b in v & b c= x )
let C be finite set ; ::_thesis: for u, v being Element of (SubstLatt (V,C)) st u [= v holds
for x being set st x in u holds
ex b being set st
( b in v & b c= x )
let u, v be Element of (SubstLatt (V,C)); ::_thesis: ( u [= v implies for x being set st x in u holds
ex b being set st
( b in v & b c= x ) )
reconsider u9 = u, v9 = v as Element of SubstitutionSet (V,C) by SUBSTLAT:def_4;
assume  u [= v ; ::_thesis: for x being set st x in u holds
ex b being set st
( b in v & b c= x )
then u = u "/\" v by LATTICES:4
.= the L_meet of (SubstLatt (V,C)) . (u,v) by LATTICES:def_2
.= mi (u9 ^ v9) by SUBSTLAT:def_4 ;
hence  for x being set st x in u holds
ex b being set st
( b in v & b c= x ) by Th4; ::_thesis: verum
end;

theorem Th24: :: HEYTING2:24
for V being set
for C being finite set
for a being Element of PFuncs (V,C)
for u, v being Element of SubstitutionSet (V,C) st ( for c being set st c in u holds
ex b being set st
( b in v & b c= c \/ a ) ) holds
ex b being set st
( b in u =>> v & b c= a )
proof
let V be set ; ::_thesis: for C being finite set
for a being Element of PFuncs (V,C)
for u, v being Element of SubstitutionSet (V,C) st ( for c being set st c in u holds
ex b being set st
( b in v & b c= c \/ a ) ) holds
ex b being set st
( b in u =>> v & b c= a )
let C be finite set ; ::_thesis: for a being Element of PFuncs (V,C)
for u, v being Element of SubstitutionSet (V,C) st ( for c being set st c in u holds
ex b being set st
( b in v & b c= c \/ a ) ) holds
ex b being set st
( b in u =>> v & b c= a )
let a be Element of PFuncs (V,C); ::_thesis: for u, v being Element of SubstitutionSet (V,C) st ( for c being set st c in u holds
ex b being set st
( b in v & b c= c \/ a ) ) holds
ex b being set st
( b in u =>> v & b c= a )
let u, v be Element of SubstitutionSet (V,C); ::_thesis: ( ( for c being set st c in u holds
ex b being set st
( b in v & b c= c \/ a ) ) implies ex b being set st
( b in u =>> v & b c= a ) )
reconsider u9 = u as Element of (SubstLatt (V,C)) by SUBSTLAT:def_4;
defpred S1[ set , set ] means ( $2 in v & $2 c= $1 \/ a );
assume A1: for b being set st b in u holds
ex c being set st
( c in v & c c= b \/ a ) ; ::_thesis: ex b being set st
( b in u =>> v & b c= a )
A2: now__::_thesis:_for_b_being_Element_of_PFuncs_(V,C)_st_b_in_u_holds_
ex_x_being_Element_of_PFuncs_(V,C)_st_S1[b,x]
let b be Element of PFuncs (V,C); ::_thesis: ( b in u implies ex x being Element of PFuncs (V,C) st S1[b,x] )
assume  b in u ; ::_thesis: ex x being Element of PFuncs (V,C) st S1[b,x]
then consider c being set  such that
A3: c in v and
A4: c c= b \/ a by A1;
 v c= PFuncs (V,C) by FINSUB_1:def_5;
then reconsider c = c as Element of PFuncs (V,C) by A3;
take x = c; ::_thesis: S1[b,x]
thus  S1[b,x] by A3, A4; ::_thesis: verum
end;
consider f9 being Element of Funcs ((PFuncs (V,C)),(PFuncs (V,C))) such that
A5: for b being Element of PFuncs (V,C) st b in u holds
S1[b,f9 . b] from FRAENKEL:sch_27(A2);
set g = f9 | u;
consider f2 being Function such that
A6: f9 = f2 and
 dom f2 = PFuncs (V,C) and
 rng f2 c= PFuncs (V,C) by FUNCT_2:def_2;
 u c= PFuncs (V,C) by FINSUB_1:def_5;
then  f9 | u is Function of u,(PFuncs (V,C)) by FUNCT_2:32;
then A7: dom (f9 | u) = u by FUNCT_2:def_1;
 for b being set st b in u holds
(f9 | u) . b in v
proof
let b be set ; ::_thesis: ( b in u implies (f9 | u) . b in v )
assume A8: b in u ; ::_thesis: (f9 | u) . b in v
 u c= PFuncs (V,C) by FINSUB_1:def_5;
then reconsider b9 = b as Element of PFuncs (V,C) by A8;
 (f9 | u) . b9 = f2 . b9 by A6, A8, FUNCT_1:49;
hence  (f9 | u) . b in v by A5, A6, A8; ::_thesis: verum
end;
then  f9 | u is Function of u,v by A7, FUNCT_2:3;
then A9: rng (f9 | u) c= v by RELAT_1:def_19;
A10: for b being set st b in u9 holds
(f9 | u) . b c= b \/ a
proof
let b be set ; ::_thesis: ( b in u9 implies (f9 | u) . b c= b \/ a )
assume A11: b in u9 ; ::_thesis: (f9 | u) . b c= b \/ a
 u c= PFuncs (V,C) by FINSUB_1:def_5;
then reconsider b9 = b as Element of PFuncs (V,C) by A11;
 (f9 | u) . b9 = f2 . b9 by A6, A11, FUNCT_1:49;
hence  (f9 | u) . b c= b \/ a by A5, A6, A11; ::_thesis: verum
end;
reconsider g = f9 | u as Element of PFuncs (u,v) by A7, A9, PARTFUN1:def_3;
set d = union  {  ((g . i) \ i) where i is Element of PFuncs (V,C) : i in u9  }  ;
A12: union  {  ((g . i) \ i) where i is Element of PFuncs (V,C) : i in u9  }  c= a
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union  {  ((g . i) \ i) where i is Element of PFuncs (V,C) : i in u9  }  or x in a )
assume  x in union  {  ((g . i) \ i) where i is Element of PFuncs (V,C) : i in u9  }  ; ::_thesis: x in a
then consider Y being set  such that
A13: x in Y and
A14: Y in  {  ((g . i) \ i) where i is Element of PFuncs (V,C) : i in u9  }  by TARSKI:def_4;
consider j being Element of PFuncs (V,C) such that
A15: Y = (g . j) \ j and
A16: j in u9 by A14;
 g . j c= j \/ a by A10, A16;
then  (g . j) \ j c= a by XBOOLE_1:43;
hence  x in a by A13, A15; ::_thesis: verum
end;
then reconsider d = union  {  ((g . i) \ i) where i is Element of PFuncs (V,C) : i in u9  }  as Element of PFuncs (V,C) by PRE_POLY:15;
take  d ; ::_thesis: ( d in u =>> v & d c= a )
 d in  {  (union  {  ((f . i) \ i) where i is Element of PFuncs (V,C) : i in u  }  ) where f is Element of PFuncs (u,v) : dom f = u  }  by A7;
hence  d in u =>> v by XBOOLE_0:def_4; ::_thesis: d c= a
thus  d c= a by A12; ::_thesis: verum
end;

theorem Th25: :: HEYTING2:25
for V being set
for C being finite set
for u, v being Element of (SubstLatt (V,C))
for a being finite Element of PFuncs (V,C) st ( for b being Element of PFuncs (V,C) st b in u holds
b tolerates a ) & u "/\" ((Atom (V,C)) . a) [= v holds
(Atom (V,C)) . a [= (StrongImpl (V,C)) . (u,v)
proof
let V be set ; ::_thesis: for C being finite set
for u, v being Element of (SubstLatt (V,C))
for a being finite Element of PFuncs (V,C) st ( for b being Element of PFuncs (V,C) st b in u holds
b tolerates a ) & u "/\" ((Atom (V,C)) . a) [= v holds
(Atom (V,C)) . a [= (StrongImpl (V,C)) . (u,v)
let C be finite set ; ::_thesis: for u, v being Element of (SubstLatt (V,C))
for a being finite Element of PFuncs (V,C) st ( for b being Element of PFuncs (V,C) st b in u holds
b tolerates a ) & u "/\" ((Atom (V,C)) . a) [= v holds
(Atom (V,C)) . a [= (StrongImpl (V,C)) . (u,v)
let u, v be Element of (SubstLatt (V,C)); ::_thesis: for a being finite Element of PFuncs (V,C) st ( for b being Element of PFuncs (V,C) st b in u holds
b tolerates a ) & u "/\" ((Atom (V,C)) . a) [= v holds
(Atom (V,C)) . a [= (StrongImpl (V,C)) . (u,v)
let a be finite Element of PFuncs (V,C); ::_thesis: ( ( for b being Element of PFuncs (V,C) st b in u holds
b tolerates a ) & u "/\" ((Atom (V,C)) . a) [= v implies (Atom (V,C)) . a [= (StrongImpl (V,C)) . (u,v) )
assume that
A1: for b being Element of PFuncs (V,C) st b in u holds
b tolerates a and
A2: u "/\" ((Atom (V,C)) . a) [= v ; ::_thesis: (Atom (V,C)) . a [= (StrongImpl (V,C)) . (u,v)
reconsider u9 = u, v9 = v, Aa = (Atom (V,C)) . a as Element of SubstitutionSet (V,C) by SUBSTLAT:def_4;
A3: now__::_thesis:_for_c_being_set_st_c_in_u_holds_
ex_e_being_set_st_
(_e_in_v_&_e_c=_c_\/_a_)
let c be set ; ::_thesis: ( c in u implies ex e being set st
( e in v & e c= c \/ a ) )
A4: a in Aa by Th23;
assume A5: c in u ; ::_thesis: ex e being set st
( e in v & e c= c \/ a )
then A6: c in u9 ;
then reconsider c9 = c as Element of PFuncs (V,C) by SETWISEO:9;
 c9 tolerates a by A1, A5;
then  c \/ a in  {  (s1 \/ t1) where s1, t1 is Element of PFuncs (V,C) : ( s1 in u9 & t1 in Aa & s1 tolerates t1 )  }  by A5, A4;
then A7: c \/ a in u9 ^ Aa by SUBSTLAT:def_3;
 c is finite by A6, Th1;
then consider b being set  such that
A8: b c= c \/ a and
A9: b in mi (u9 ^ Aa) by A7, SUBSTLAT:10;
 b in the L_meet of (SubstLatt (V,C)) . (u,((Atom (V,C)) . a)) by A9, SUBSTLAT:def_4;
then  b in u "/\" ((Atom (V,C)) . a) by LATTICES:def_2;
then consider d being set  such that
A10: d in v and
A11: d c= b by A2, Lm9;
take e = d; ::_thesis: ( e in v & e c= c \/ a )
thus  e in v by A10; ::_thesis: e c= c \/ a
thus  e c= c \/ a by A8, A11, XBOOLE_1:1; ::_thesis: verum
end;
now__::_thesis:_for_c_being_set_st_c_in_(Atom_(V,C))_._a_holds_
ex_e_being_set_st_
(_e_in_(StrongImpl_(V,C))_._(u,v)_&_e_c=_c_)
let c be set ; ::_thesis: ( c in (Atom (V,C)) . a implies ex e being set st
( e in (StrongImpl (V,C)) . (u,v) & e c= c ) )
assume A12: c in (Atom (V,C)) . a ; ::_thesis: ex e being set st
( e in (StrongImpl (V,C)) . (u,v) & e c= c )
then  c = a by Th21;
then consider b being set  such that
A13: b in u9 =>> v9 and
A14: b c= c by A3, Th24;
 c in Aa by A12;
then  c is finite by Th1;
then consider d being set  such that
A15: d c= b and
A16: d in mi (u9 =>> v9) by A13, A14, SUBSTLAT:10;
take e = d; ::_thesis: ( e in (StrongImpl (V,C)) . (u,v) & e c= c )
thus  e in (StrongImpl (V,C)) . (u,v) by A16, Def5; ::_thesis: e c= c
thus  e c= c by A14, A15, XBOOLE_1:1; ::_thesis: verum
end;
hence  (Atom (V,C)) . a [= (StrongImpl (V,C)) . (u,v) by Lm8; ::_thesis: verum
end;

deffunc H1( set , set ) ->  Element of bool [:[: the carrier of (SubstLatt ($1,$2)), the carrier of (SubstLatt ($1,$2)):], the carrier of (SubstLatt ($1,$2)):] = the L_meet of (SubstLatt ($1,$2));

theorem Th26: :: HEYTING2:26
for V being set
for C being finite set
for u being Element of (SubstLatt (V,C)) holds u "/\" ((pseudo_compl (V,C)) . u) = Bottom (SubstLatt (V,C))
proof
let V be set ; ::_thesis: for C being finite set
for u being Element of (SubstLatt (V,C)) holds u "/\" ((pseudo_compl (V,C)) . u) = Bottom (SubstLatt (V,C))
let C be finite set ; ::_thesis: for u being Element of (SubstLatt (V,C)) holds u "/\" ((pseudo_compl (V,C)) . u) = Bottom (SubstLatt (V,C))
let u be Element of (SubstLatt (V,C)); ::_thesis: u "/\" ((pseudo_compl (V,C)) . u) = Bottom (SubstLatt (V,C))
reconsider u9 = u as Element of SubstitutionSet (V,C) by SUBSTLAT:def_4;
thus u "/\" ((pseudo_compl (V,C)) . u) = H1(V,C) . (u,((pseudo_compl (V,C)) . u)) by LATTICES:def_2
.= H1(V,C) . (u,(mi (- u9))) by Def4
.= mi (u9 ^ (mi (- u9))) by SUBSTLAT:def_4
.= mi (u9 ^ (- u9)) by SUBSTLAT:20
.= Bottom (SubstLatt (V,C)) by Th12 ; ::_thesis: verum
end;

theorem Th27: :: HEYTING2:27
for V being set
for C being finite set
for u, v being Element of (SubstLatt (V,C)) holds u "/\" ((StrongImpl (V,C)) . (u,v)) [= v
proof
let V be set ; ::_thesis: for C being finite set
for u, v being Element of (SubstLatt (V,C)) holds u "/\" ((StrongImpl (V,C)) . (u,v)) [= v
let C be finite set ; ::_thesis: for u, v being Element of (SubstLatt (V,C)) holds u "/\" ((StrongImpl (V,C)) . (u,v)) [= v
let u, v be Element of (SubstLatt (V,C)); ::_thesis: u "/\" ((StrongImpl (V,C)) . (u,v)) [= v
now__::_thesis:_for_a_being_set_st_a_in_u_"/\"_((StrongImpl_(V,C))_._(u,v))_holds_
ex_b_being_set_st_
(_b_in_v_&_b_c=_a_)
reconsider u9 = u, v9 = v as Element of SubstitutionSet (V,C) by SUBSTLAT:def_4;
let a be set ; ::_thesis: ( a in u "/\" ((StrongImpl (V,C)) . (u,v)) implies ex b being set st
( b in v & b c= a ) )
assume A1: a in u "/\" ((StrongImpl (V,C)) . (u,v)) ; ::_thesis: ex b being set st
( b in v & b c= a )
u "/\" ((StrongImpl (V,C)) . (u,v)) = H1(V,C) . (u,((StrongImpl (V,C)) . (u,v))) by LATTICES:def_2
.= H1(V,C) . (u,(mi (u9 =>> v9))) by Def5
.= mi (u9 ^ (mi (u9 =>> v9))) by SUBSTLAT:def_4
.= mi (u9 ^ (u9 =>> v9)) by SUBSTLAT:20 ;
then  a in u9 ^ (u9 =>> v9) by A1, SUBSTLAT:6;
hence  ex b being set st
( b in v & b c= a ) by Lm3; ::_thesis: verum
end;
hence  u "/\" ((StrongImpl (V,C)) . (u,v)) [= v by Lm8; ::_thesis: verum
end;

Lm10: now__::_thesis:_for_V_being_set_
for_C_being_finite_set_
for_u,_v_being_Element_of_(SubstLatt_(V,C))_holds_
(_u_"/\"_H2(u,v)_[=_v_&_(_for_w_being_Element_of_(SubstLatt_(V,C))_st_u_"/\"_v_[=_w_holds_
v_[=_H2(u,w)_)_)
let V be set ; ::_thesis: for C being finite set
for u, v being Element of (SubstLatt (V,C)) holds
( u "/\" H2(u,v) [= v & ( for w being Element of (SubstLatt (V,C)) st u "/\" v [= w holds
v [= H2(u,w) ) )
let C be finite set ; ::_thesis: for u, v being Element of (SubstLatt (V,C)) holds
( u "/\" H2(u,v) [= v & ( for w being Element of (SubstLatt (V,C)) st u "/\" v [= w holds
v [= H2(u,w) ) )
let u, v be Element of (SubstLatt (V,C)); ::_thesis: ( u "/\" H2(u,v) [= v & ( for w being Element of (SubstLatt (V,C)) st u "/\" v [= w holds
v [= H2(u,w) ) )
deffunc H2( Element of (SubstLatt (V,C)), Element of (SubstLatt (V,C))) ->  Element of the carrier of (SubstLatt (V,C)) = FinJoin ((SUB $1),(H1(V,C) .: ((pseudo_compl (V,C)),((StrongImpl (V,C)) [:] ((diff $1),$2)))));
set Psi = H1(V,C) .: ((pseudo_compl (V,C)),((StrongImpl (V,C)) [:] ((diff u),v)));
reconsider v9 = v as Element of SubstitutionSet (V,C) by SUBSTLAT:def_4;
A1: now__::_thesis:_for_w_being_Element_of_(SubstLatt_(V,C))_st_w_in_SUB_u_holds_
(H1(V,C)_[;]_(u,(H1(V,C)_.:_((pseudo_compl_(V,C)),((StrongImpl_(V,C))_[:]_((diff_u),v))))))_._w_[=_v
let w be Element of (SubstLatt (V,C)); ::_thesis: ( w in SUB u implies (H1(V,C) [;] (u,(H1(V,C) .: ((pseudo_compl (V,C)),((StrongImpl (V,C)) [:] ((diff u),v)))))) . w [= v )
set u2 = (diff u) . w;
set pc = (pseudo_compl (V,C)) . w;
set si = (StrongImpl (V,C)) . (((diff u) . w),v);
A2: w "/\" (((pseudo_compl (V,C)) . w) "/\" ((StrongImpl (V,C)) . (((diff u) . w),v))) = (w "/\" ((pseudo_compl (V,C)) . w)) "/\" ((StrongImpl (V,C)) . (((diff u) . w),v)) by LATTICES:def_7
.= (Bottom (SubstLatt (V,C))) "/\" ((StrongImpl (V,C)) . (((diff u) . w),v)) by Th26
.= Bottom (SubstLatt (V,C)) ;
assume  w in SUB u ; ::_thesis: (H1(V,C) [;] (u,(H1(V,C) .: ((pseudo_compl (V,C)),((StrongImpl (V,C)) [:] ((diff u),v)))))) . w [= v
then A3: w "\/" ((diff u) . w) = u by Lm5;
(H1(V,C) [;] (u,(H1(V,C) .: ((pseudo_compl (V,C)),((StrongImpl (V,C)) [:] ((diff u),v)))))) . w = H1(V,C) . (u,((H1(V,C) .: ((pseudo_compl (V,C)),((StrongImpl (V,C)) [:] ((diff u),v)))) . w)) by FUNCOP_1:53
.= u "/\" ((H1(V,C) .: ((pseudo_compl (V,C)),((StrongImpl (V,C)) [:] ((diff u),v)))) . w) by LATTICES:def_2
.= u "/\" (H1(V,C) . (((pseudo_compl (V,C)) . w),(((StrongImpl (V,C)) [:] ((diff u),v)) . w))) by FUNCOP_1:37
.= u "/\" (((pseudo_compl (V,C)) . w) "/\" (((StrongImpl (V,C)) [:] ((diff u),v)) . w)) by LATTICES:def_2
.= u "/\" (((pseudo_compl (V,C)) . w) "/\" ((StrongImpl (V,C)) . (((diff u) . w),v))) by FUNCOP_1:48
.= (w "/\" (((pseudo_compl (V,C)) . w) "/\" ((StrongImpl (V,C)) . (((diff u) . w),v)))) "\/" (((diff u) . w) "/\" (((pseudo_compl (V,C)) . w) "/\" ((StrongImpl (V,C)) . (((diff u) . w),v)))) by A3, LATTICES:def_11
.= ((diff u) . w) "/\" (((StrongImpl (V,C)) . (((diff u) . w),v)) "/\" ((pseudo_compl (V,C)) . w)) by A2, LATTICES:14
.= (((diff u) . w) "/\" ((StrongImpl (V,C)) . (((diff u) . w),v))) "/\" ((pseudo_compl (V,C)) . w) by LATTICES:def_7 ;
then A4: (H1(V,C) [;] (u,(H1(V,C) .: ((pseudo_compl (V,C)),((StrongImpl (V,C)) [:] ((diff u),v)))))) . w [= ((diff u) . w) "/\" ((StrongImpl (V,C)) . (((diff u) . w),v)) by LATTICES:6;
 ((diff u) . w) "/\" ((StrongImpl (V,C)) . (((diff u) . w),v)) [= v by Th27;
hence  (H1(V,C) [;] (u,(H1(V,C) .: ((pseudo_compl (V,C)),((StrongImpl (V,C)) [:] ((diff u),v)))))) . w [= v by A4, LATTICES:7; ::_thesis: verum
end;
 u "/\" H2(u,v) = FinJoin ((SUB u),(H1(V,C) [;] (u,(H1(V,C) .: ((pseudo_compl (V,C)),((StrongImpl (V,C)) [:] ((diff u),v))))))) by LATTICE2:66;
hence  u "/\" H2(u,v) [= v by A1, LATTICE2:54; ::_thesis: for w being Element of (SubstLatt (V,C)) st u "/\" v [= w holds
v [= H2(u,w)
let w be Element of (SubstLatt (V,C)); ::_thesis: ( u "/\" v [= w implies v [= H2(u,w) )
assume A5: u "/\" v [= w ; ::_thesis: v [= H2(u,w)
A6: v = FinJoin (v9,(Atom (V,C))) by Th19;
then A7: u "/\" v = FinJoin (v9,(H1(V,C) [;] (u,(Atom (V,C))))) by LATTICE2:66;
now__::_thesis:_for_a_being_Element_of_PFuncs_(V,C)_st_a_in_v9_holds_
(Atom_(V,C))_._a_[=_H2(u,w)
set pf = pseudo_compl (V,C);
set sf = (StrongImpl (V,C)) [:] ((diff u),w);
let a be Element of PFuncs (V,C); ::_thesis: ( a in v9 implies (Atom (V,C)) . a [= H2(u,w) )
reconsider SA = {.a.} as Element of Fin (PFuncs (V,C)) ;
consider v being Element of SubstitutionSet (V,C) such that
A8: v in SUB u and
A9: v ^ SA = {} and
A10: for b being Element of PFuncs (V,C) st b in (diff u) . v holds
b tolerates a by Lm6;
assume A11: a in v9 ; ::_thesis: (Atom (V,C)) . a [= H2(u,w)
then A12: a is finite by Th1;
reconsider v9 = v as Element of (SubstLatt (V,C)) by SUBSTLAT:def_4;
set dv = (diff u) . v9;
 (H1(V,C) [;] (u,(Atom (V,C)))) . a [= w by A7, A5, A11, LATTICE2:31;
then  H1(V,C) . (u,((Atom (V,C)) . a)) [= w by FUNCOP_1:53;
then A13: u "/\" ((Atom (V,C)) . a) [= w by LATTICES:def_2;
 a is finite by A11, Th1;
then reconsider SS = {a} as Element of SubstitutionSet (V,C) by Th2;
 v ^ SS = {} by A9;
then A14: (Atom (V,C)) . a [= (pseudo_compl (V,C)) . v9 by Th22;
 ((diff u) . v9) "/\" ((Atom (V,C)) . a) [= u "/\" ((Atom (V,C)) . a) by Th20, LATTICES:9;
then  ((diff u) . v9) "/\" ((Atom (V,C)) . a) [= w by A13, LATTICES:7;
then  (Atom (V,C)) . a [= (StrongImpl (V,C)) . (((diff u) . v9),w) by A10, A12, Th25;
then A15: (Atom (V,C)) . a [= ((StrongImpl (V,C)) [:] ((diff u),w)) . v9 by FUNCOP_1:48;
((pseudo_compl (V,C)) . v9) "/\" (((StrongImpl (V,C)) [:] ((diff u),w)) . v9) = H1(V,C) . (((pseudo_compl (V,C)) . v9),(((StrongImpl (V,C)) [:] ((diff u),w)) . v9)) by LATTICES:def_2
.= (H1(V,C) .: ((pseudo_compl (V,C)),((StrongImpl (V,C)) [:] ((diff u),w)))) . v9 by FUNCOP_1:37 ;
then  (Atom (V,C)) . a [= (H1(V,C) .: ((pseudo_compl (V,C)),((StrongImpl (V,C)) [:] ((diff u),w)))) . v9 by A14, A15, FILTER_0:7;
hence  (Atom (V,C)) . a [= H2(u,w) by A8, LATTICE2:29; ::_thesis: verum
end;
hence  v [= H2(u,w) by A6, LATTICE2:54; ::_thesis: verum
end;

Lm11:  for V being set
for C being finite set holds SubstLatt (V,C) is implicative
proof
let V be set ; ::_thesis: for C being finite set holds SubstLatt (V,C) is implicative
let C be finite set ; ::_thesis: SubstLatt (V,C) is implicative
let p, q be Element of (SubstLatt (V,C)); :: according to FILTER_0:def_6 ::_thesis: ex b1 being Element of the carrier of (SubstLatt (V,C)) st
( p "/\" b1 [= q & ( for b2 being Element of the carrier of (SubstLatt (V,C)) holds
( not p "/\" b2 [= q or b2 [= b1 ) ) )
take r = FinJoin ((SUB p),(H1(V,C) .: ((pseudo_compl (V,C)),((StrongImpl (V,C)) [:] ((diff p),q))))); ::_thesis: ( p "/\" r [= q & ( for b1 being Element of the carrier of (SubstLatt (V,C)) holds
( not p "/\" b1 [= q or b1 [= r ) ) )
thus  ( p "/\" r [= q & ( for r1 being Element of (SubstLatt (V,C)) st p "/\" r1 [= q holds
r1 [= r ) ) by Lm10; ::_thesis: verum
end;

registration
let V be set ;
let C be finite set ;
cluster SubstLatt (V,C) ->  implicative ;
coherence
 SubstLatt (V,C) is implicative by Lm11;
end;

theorem :: HEYTING2:28
for V being set
for C being finite set
for u, v being Element of (SubstLatt (V,C)) holds u => v = FinJoin ((SUB u),( the L_meet of (SubstLatt (V,C)) .: ((pseudo_compl (V,C)),((StrongImpl (V,C)) [:] ((diff u),v)))))
proof
let V be set ; ::_thesis: for C being finite set
for u, v being Element of (SubstLatt (V,C)) holds u => v = FinJoin ((SUB u),( the L_meet of (SubstLatt (V,C)) .: ((pseudo_compl (V,C)),((StrongImpl (V,C)) [:] ((diff u),v)))))
let C be finite set ; ::_thesis: for u, v being Element of (SubstLatt (V,C)) holds u => v = FinJoin ((SUB u),( the L_meet of (SubstLatt (V,C)) .: ((pseudo_compl (V,C)),((StrongImpl (V,C)) [:] ((diff u),v)))))
let u, v be Element of (SubstLatt (V,C)); ::_thesis: u => v = FinJoin ((SUB u),( the L_meet of (SubstLatt (V,C)) .: ((pseudo_compl (V,C)),((StrongImpl (V,C)) [:] ((diff u),v)))))
deffunc H2( Element of (SubstLatt (V,C)), Element of (SubstLatt (V,C))) ->  Element of the carrier of (SubstLatt (V,C)) = FinJoin ((SUB $1),(H1(V,C) .: ((pseudo_compl (V,C)),((StrongImpl (V,C)) [:] ((diff $1),$2)))));
A1: for w being Element of (SubstLatt (V,C)) st u "/\" w [= v holds
w [= H2(u,v) by Lm10;
 u "/\" H2(u,v) [= v by Lm10;
hence  u => v = FinJoin ((SUB u),( the L_meet of (SubstLatt (V,C)) .: ((pseudo_compl (V,C)),((StrongImpl (V,C)) [:] ((diff u),v))))) by A1, FILTER_0:def_7; ::_thesis: verum
end;