:: HEYTING2 semantic presentation

registration
let c1, c2 be set ;
cluster {[a1,a2]} -> Relation-like Function-like ;
coherence
( {[c1,c2]} is Function-like & {[c1,c2]} is Relation-like )
proof end;
end;

theorem Th1: :: HEYTING2:1
for b1, b2 being non empty set ex b3 being Element of PFuncs b1,b2 st b3 <> {}
proof end;

theorem Th2: :: HEYTING2:2
for b1, b2, b3, b4 being set st b4 in SubstitutionSet b1,b2 & b3 in b4 holds
b3 is finite Function
proof end;

theorem Th3: :: HEYTING2:3
for b1, b2 being set
for b3 being Element of PFuncs b1,b2
for b4 being set st b4 c= b3 holds
b4 in PFuncs b1,b2
proof end;

Lemma3: for b1, b2, b3 being set st b1 = b2 \/ b3 & b1 c= b2 holds
b1 = b2
proof end;

theorem Th4: :: HEYTING2:4
for b1, b2 being set holds PFuncs b1,b2 c= bool [:b1,b2:]
proof end;

theorem Th5: :: HEYTING2:5
for b1, b2 being set st b1 is finite & b2 is finite holds
PFuncs b1,b2 is finite
proof end;

registration
cluster non empty finite functional set ;
existence
ex b1 being set st
( b1 is functional & b1 is finite & not b1 is empty )
proof end;
end;

theorem Th6: :: HEYTING2:6
for b1, b2 being set
for b3 being finite Element of PFuncs b1,b2 holds {b3} in SubstitutionSet b1,b2
proof end;

theorem Th7: :: HEYTING2:7
for b1, b2 being set
for b3, b4 being Element of SubstitutionSet b1,b2 st b3 ^ b4 = b3 holds
for b5 being set st b5 in b3 holds
ex b6 being set st
( b6 in b4 & b6 c= b5 )
proof end;

theorem Th8: :: HEYTING2:8
for b1, b2 being set
for b3, b4 being Element of SubstitutionSet b1,b2 st mi (b3 ^ b4) = b3 holds
for b5 being set st b5 in b3 holds
ex b6 being set st
( b6 in b4 & b6 c= b5 )
proof end;

theorem Th9: :: HEYTING2:9
for b1, b2 being set
for b3, b4 being Element of SubstitutionSet b1,b2 st ( for b5 being set st b5 in b3 holds
ex b6 being set st
( b6 in b4 & b6 c= b5 ) ) holds
mi (b3 ^ b4) = b3
proof end;

definition
let c1 be set ;
let c2 be finite set ;
let c3 be Element of Fin (PFuncs c1,c2);
func Involved c3 -> set means :Def1: :: HEYTING2:def 1
for b1 being set holds
( b1 in a4 iff ex b2 being finite Function st
( b2 in a3 & b1 in dom b2 ) );
existence
ex b1 being set st
for b2 being set holds
( b2 in b1 iff ex b3 being finite Function st
( b3 in c3 & b2 in dom b3 ) )
proof end;
uniqueness
for b1, b2 being set st ( for b3 being set holds
( b3 in b1 iff ex b4 being finite Function st
( b4 in c3 & b3 in dom b4 ) ) ) & ( for b3 being set holds
( b3 in b2 iff ex b4 being finite Function st
( b4 in c3 & b3 in dom b4 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines Involved HEYTING2:def 1 :
for b1 being set
for b2 being finite set
for b3 being Element of Fin (PFuncs b1,b2)
for b4 being set holds
( b4 = Involved b3 iff for b5 being set holds
( b5 in b4 iff ex b6 being finite Function st
( b6 in b3 & b5 in dom b6 ) ) );

theorem Th10: :: HEYTING2:10
for b1 being set
for b2 being finite set
for b3 being Element of Fin (PFuncs b1,b2) holds Involved b3 c= b1
proof end;

Lemma11: for b1 being set
for b2 being finite set
for b3 being non empty Element of Fin (PFuncs b1,b2) holds Involved b3 is finite
proof end;

theorem Th11: :: HEYTING2:11
for b1 being set
for b2 being finite set
for b3 being Element of Fin (PFuncs b1,b2) st b3 = {} holds
Involved b3 = {}
proof end;

theorem Th12: :: HEYTING2:12
for b1 being set
for b2 being finite set
for b3 being Element of Fin (PFuncs b1,b2) holds Involved b3 is finite
proof end;

theorem Th13: :: HEYTING2:13
for b1 being finite set
for b2 being Element of Fin (PFuncs {} ,b1) holds Involved b2 = {}
proof end;

definition
let c1 be set ;
let c2 be finite set ;
let c3 be Element of Fin (PFuncs c1,c2);
func - c3 -> Element of Fin (PFuncs a1,a2) equals :: HEYTING2:def 2
{ b1 where B is Element of PFuncs (Involved a3),a2 : for b1 being Element of PFuncs a1,a2 st b2 in a3 holds
not b1 tolerates b2 } ;
coherence
{ b1 where B is Element of PFuncs (Involved c3),c2 : for b1 being Element of PFuncs c1,c2 st b2 in c3 holds
not b1 tolerates b2 } is Element of Fin (PFuncs c1,c2)
proof end;
end;

:: deftheorem Def2 defines - HEYTING2:def 2 :
for b1 being set
for b2 being finite set
for b3 being Element of Fin (PFuncs b1,b2) holds - b3 = { b4 where B is Element of PFuncs (Involved b3),b2 : for b1 being Element of PFuncs b1,b2 st b5 in b3 holds
not b4 tolerates b5 } ;

theorem Th14: :: HEYTING2:14
for b1 being set
for b2 being finite set
for b3 being Element of SubstitutionSet b1,b2 holds b3 ^ (- b3) = {}
proof end;

theorem Th15: :: HEYTING2:15
for b1 being set
for b2 being finite set
for b3 being Element of SubstitutionSet b1,b2 st b3 = {} holds
- b3 = {{} }
proof end;

theorem Th16: :: HEYTING2:16
for b1 being set
for b2 being finite set
for b3 being Element of SubstitutionSet b1,b2 st b3 = {{} } holds
- b3 = {}
proof end;

theorem Th17: :: HEYTING2:17
for b1 being set
for b2 being finite set
for b3 being Element of SubstitutionSet b1,b2 holds mi (b3 ^ (- b3)) = Bottom (SubstLatt b1,b2)
proof end;

theorem Th18: :: HEYTING2:18
for b1 being non empty set
for b2 being non empty finite set
for b3 being Element of SubstitutionSet b1,b2 st b3 = {} holds
mi (- b3) = Top (SubstLatt b1,b2)
proof end;

theorem Th19: :: HEYTING2:19
for b1 being set
for b2 being finite set
for b3 being Element of SubstitutionSet b1,b2
for b4 being Element of PFuncs b1,b2
for b5 being Element of SubstitutionSet b1,b2 st b5 = {b4} & b3 ^ b5 = {} holds
ex b6 being finite set st
( b6 in - b3 & b6 c= b4 )
proof end;

definition
let c1 be set ;
let c2 be finite set ;
let c3, c4 be Element of Fin (PFuncs c1,c2);
func c3 =>> c4 -> Element of Fin (PFuncs a1,a2) equals :: HEYTING2:def 3
(PFuncs a1,a2) /\ { (union { ((b1 . b2) \ b2) where B is Element of PFuncs a1,a2 : b2 in a3 } ) where B is Element of PFuncs a3,a4 : dom b1 = a3 } ;
coherence
(PFuncs c1,c2) /\ { (union { ((b1 . b2) \ b2) where B is Element of PFuncs c1,c2 : b2 in c3 } ) where B is Element of PFuncs c3,c4 : dom b1 = c3 } is Element of Fin (PFuncs c1,c2)
proof end;
end;

:: deftheorem Def3 defines =>> HEYTING2:def 3 :
for b1 being set
for b2 being finite set
for b3, b4 being Element of Fin (PFuncs b1,b2) holds b3 =>> b4 = (PFuncs b1,b2) /\ { (union { ((b5 . b6) \ b6) where B is Element of PFuncs b1,b2 : b6 in b3 } ) where B is Element of PFuncs b3,b4 : dom b5 = b3 } ;

theorem Th20: :: HEYTING2:20
for b1 being set
for b2 being finite set
for b3, b4 being Element of Fin (PFuncs b1,b2)
for b5 being set st b5 in b3 =>> b4 holds
ex b6 being PartFunc of b3,b4 st
( b5 = union { ((b6 . b7) \ b7) where B is Element of PFuncs b1,b2 : b7 in b3 } & dom b6 = b3 )
proof end;

Lemma19: for b1, b2 being set
for b3 being finite set
for b4 being Element of Fin (PFuncs b2,b3)
for b5 being Element of SubstitutionSet b2,b3 st b1 in b4 ^ (b4 =>> b5) holds
ex b6 being set st
( b6 in b5 & b6 c= b1 )
proof end;

theorem Th21: :: HEYTING2:21
for b1 being set
for b2 being finite set
for b3 being Element of Fin (PFuncs b1,b2) st b3 = {} holds
b3 =>> b3 = {{} }
proof end;

Lemma20: for b1 being set
for b2 being finite set
for b3 being Element of SubstitutionSet b1,b2
for b4 being set st b4 c= b3 holds
b4 in SubstitutionSet b1,b2
proof end;

theorem Th22: :: HEYTING2:22
for b1 being set
for b2 being finite set
for b3 being Element of (SubstLatt b1,b2)
for b4 being set st b4 c= b3 holds
b4 is Element of (SubstLatt b1,b2)
proof end;

definition
let c1 be set ;
let c2 be finite set ;
func pseudo_compl c1,c2 -> UnOp of the carrier of (SubstLatt a1,a2) means :Def4: :: HEYTING2:def 4
for b1 being Element of (SubstLatt a1,a2)
for b2 being Element of SubstitutionSet a1,a2 st b2 = b1 holds
a3 . b1 = mi (- b2);
existence
ex b1 being UnOp of the carrier of (SubstLatt c1,c2) st
for b2 being Element of (SubstLatt c1,c2)
for b3 being Element of SubstitutionSet c1,c2 st b3 = b2 holds
b1 . b2 = mi (- b3)
proof end;
correctness
uniqueness
for b1, b2 being UnOp of the carrier of (SubstLatt c1,c2) st ( for b3 being Element of (SubstLatt c1,c2)
for b4 being Element of SubstitutionSet c1,c2 st b4 = b3 holds
b1 . b3 = mi (- b4) ) & ( for b3 being Element of (SubstLatt c1,c2)
for b4 being Element of SubstitutionSet c1,c2 st b4 = b3 holds
b2 . b3 = mi (- b4) ) holds
b1 = b2;
proof end;
func StrongImpl c1,c2 -> BinOp of the carrier of (SubstLatt a1,a2) means :Def5: :: HEYTING2:def 5
for b1, b2 being Element of (SubstLatt a1,a2)
for b3, b4 being Element of SubstitutionSet a1,a2 st b3 = b1 & b4 = b2 holds
a3 . b1,b2 = mi (b3 =>> b4);
existence
ex b1 being BinOp of the carrier of (SubstLatt c1,c2) st
for b2, b3 being Element of (SubstLatt c1,c2)
for b4, b5 being Element of SubstitutionSet c1,c2 st b4 = b2 & b5 = b3 holds
b1 . b2,b3 = mi (b4 =>> b5)
proof end;
correctness
uniqueness
for b1, b2 being BinOp of the carrier of (SubstLatt c1,c2) st ( for b3, b4 being Element of (SubstLatt c1,c2)
for b5, b6 being Element of SubstitutionSet c1,c2 st b5 = b3 & b6 = b4 holds
b1 . b3,b4 = mi (b5 =>> b6) ) & ( for b3, b4 being Element of (SubstLatt c1,c2)
for b5, b6 being Element of SubstitutionSet c1,c2 st b5 = b3 & b6 = b4 holds
b2 . b3,b4 = mi (b5 =>> b6) ) holds
b1 = b2;
proof end;
let c3 be Element of (SubstLatt c1,c2);
func SUB c3 -> Element of Fin the carrier of (SubstLatt a1,a2) equals :: HEYTING2:def 6
 bool a3;
coherence
bool c3 is Element of Fin the carrier of (SubstLatt c1,c2)
proof end;
correctness
;
func diff c3 -> UnOp of the carrier of (SubstLatt a1,a2) means :Def7: :: HEYTING2:def 7
for b1 being Element of (SubstLatt a1,a2) holds a4 . b1 = a3 \ b1;
existence
ex b1 being UnOp of the carrier of (SubstLatt c1,c2) st
for b2 being Element of (SubstLatt c1,c2) holds b1 . b2 = c3 \ b2
proof end;
correctness
uniqueness
for b1, b2 being UnOp of the carrier of (SubstLatt c1,c2) st ( for b3 being Element of (SubstLatt c1,c2) holds b1 . b3 = c3 \ b3 ) & ( for b3 being Element of (SubstLatt c1,c2) holds b2 . b3 = c3 \ b3 ) holds
b1 = b2;
proof end;
end;

:: deftheorem Def4 defines pseudo_compl HEYTING2:def 4 :
for b1 being set
for b2 being finite set
for b3 being UnOp of the carrier of (SubstLatt b1,b2) holds
( b3 = pseudo_compl b1,b2 iff for b4 being Element of (SubstLatt b1,b2)
for b5 being Element of SubstitutionSet b1,b2 st b5 = b4 holds
b3 . b4 = mi (- b5) );

:: deftheorem Def5 defines StrongImpl HEYTING2:def 5 :
for b1 being set
for b2 being finite set
for b3 being BinOp of the carrier of (SubstLatt b1,b2) holds
( b3 = StrongImpl b1,b2 iff for b4, b5 being Element of (SubstLatt b1,b2)
for b6, b7 being Element of SubstitutionSet b1,b2 st b6 = b4 & b7 = b5 holds
b3 . b4,b5 = mi (b6 =>> b7) );

:: deftheorem Def6 defines SUB HEYTING2:def 6 :
for b1 being set
for b2 being finite set
for b3 being Element of (SubstLatt b1,b2) holds SUB b3 = bool b3;

:: deftheorem Def7 defines diff HEYTING2:def 7 :
for b1 being set
for b2 being finite set
for b3 being Element of (SubstLatt b1,b2)
for b4 being UnOp of the carrier of (SubstLatt b1,b2) holds
( b4 = diff b3 iff for b5 being Element of (SubstLatt b1,b2) holds b4 . b5 = b3 \ b5 );

Lemma25: for b1 being set
for b2 being finite set
for b3, b4 being Element of (SubstLatt b1,b2) st b3 in SUB b4 holds
b3 "\/" ((diff b4) . b3) = b4
proof end;

Lemma26: for b1 being set
for b2 being finite set
for b3 being Element of (SubstLatt b1,b2)
for b4 being Element of PFuncs b1,b2
for b5 being Element of Fin (PFuncs b1,b2) st b4 is finite & b5 = {b4} holds
ex b6 being Element of SubstitutionSet b1,b2 st
( b6 in SUB b3 & b6 ^ b5 = {} & ( for b7 being Element of PFuncs b1,b2 st b7 in (diff b3) . b6 holds
b7 tolerates b4 ) )
proof end;

definition
let c1 be set ;
let c2 be finite set ;
func Atom c1,c2 -> Function of PFuncs a1,a2,the carrier of (SubstLatt a1,a2) means :Def8: :: HEYTING2:def 8
for b1 being Element of PFuncs a1,a2 holds a3 . b1 = mi {b1};
existence
ex b1 being Function of PFuncs c1,c2,the carrier of (SubstLatt c1,c2) st
for b2 being Element of PFuncs c1,c2 holds b1 . b2 = mi {b2}
proof end;
correctness
uniqueness
for b1, b2 being Function of PFuncs c1,c2,the carrier of (SubstLatt c1,c2) st ( for b3 being Element of PFuncs c1,c2 holds b1 . b3 = mi {b3} ) & ( for b3 being Element of PFuncs c1,c2 holds b2 . b3 = mi {b3} ) holds
b1 = b2;
proof end;
end;

:: deftheorem Def8 defines Atom HEYTING2:def 8 :
for b1 being set
for b2 being finite set
for b3 being Function of PFuncs b1,b2,the carrier of (SubstLatt b1,b2) holds
( b3 = Atom b1,b2 iff for b4 being Element of PFuncs b1,b2 holds b3 . b4 = mi {b4} );

Lemma28: for b1 being set
for b2 being finite set
for b3 being Element of PFuncs b1,b2 st b3 is finite holds
(Atom b1,b2) . b3 = {b3}
proof end;

theorem Th23: :: HEYTING2:23
for b1 being set
for b2 being finite set
for b3 being Element of SubstitutionSet b1,b2 holds FinJoin b3,(Atom b1,b2) = FinUnion b3,(singleton (PFuncs b1,b2))
proof end;

theorem Th24: :: HEYTING2:24
for b1 being set
for b2 being finite set
for b3 being Element of SubstitutionSet b1,b2 holds b3 = FinJoin b3,(Atom b1,b2)
proof end;

Lemma31: for b1 being set
for b2 being finite set
for b3, b4 being Element of (SubstLatt b1,b2) st ( for b5 being set st b5 in b3 holds
ex b6 being set st
( b6 in b4 & b6 c= b5 ) ) holds
b3 [= b4
proof end;

theorem Th25: :: HEYTING2:25
for b1 being set
for b2 being finite set
for b3, b4 being Element of (SubstLatt b1,b2) holds (diff b3) . b4 [= b3
proof end;

theorem Th26: :: HEYTING2:26
for b1 being set
for b2 being finite set
for b3 being Element of PFuncs b1,b2 st b3 is finite holds
for b4 being set st b4 in (Atom b1,b2) . b3 holds
b4 = b3
proof end;

theorem Th27: :: HEYTING2:27
for b1 being set
for b2 being finite set
for b3 being Element of (SubstLatt b1,b2)
for b4, b5 being Element of SubstitutionSet b1,b2
for b6 being Element of PFuncs b1,b2 st b4 = {b6} & b5 = b3 & b5 ^ b4 = {} holds
(Atom b1,b2) . b6 [= (pseudo_compl b1,b2) . b3
proof end;

theorem Th28: :: HEYTING2:28
for b1 being set
for b2 being finite set
for b3 being finite Element of PFuncs b1,b2 holds b3 in (Atom b1,b2) . b3
proof end;

Lemma36: for b1 being set
for b2 being finite set
for b3, b4 being Element of (SubstLatt b1,b2) st b3 [= b4 holds
for b5 being set st b5 in b3 holds
ex b6 being set st
( b6 in b4 & b6 c= b5 )
proof end;

theorem Th29: :: HEYTING2:29
for b1 being set
for b2 being finite set
for b3 being Element of PFuncs b1,b2
for b4, b5 being Element of SubstitutionSet b1,b2 st ( for b6 being set st b6 in b4 holds
ex b7 being set st
( b7 in b5 & b7 c= b6 \/ b3 ) ) holds
ex b6 being set st
( b6 in b4 =>> b5 & b6 c= b3 )
proof end;

theorem Th30: :: HEYTING2:30
for b1 being set
for b2 being finite set
for b3, b4 being Element of (SubstLatt b1,b2)
for b5 being finite Element of PFuncs b1,b2 st ( for b6 being Element of PFuncs b1,b2 st b6 in b3 holds
b6 tolerates b5 ) & b3 "/\" ((Atom b1,b2) . b5) [= b4 holds
(Atom b1,b2) . b5 [= (StrongImpl b1,b2) . b3,b4
proof end;

deffunc H1( set , set ) -> Relation of [:the carrier of (SubstLatt a1,a2),the carrier of (SubstLatt a1,a2):],the carrier of (SubstLatt a1,a2) = the L_meet of (SubstLatt a1,a2);

theorem Th31: :: HEYTING2:31
for b1 being set
for b2 being finite set
for b3 being Element of (SubstLatt b1,b2) holds b3 "/\" ((pseudo_compl b1,b2) . b3) = Bottom (SubstLatt b1,b2)
proof end;

theorem Th32: :: HEYTING2:32
for b1 being set
for b2 being finite set
for b3, b4 being Element of (SubstLatt b1,b2) holds b3 "/\" ((StrongImpl b1,b2) . b3,b4) [= b4
proof end;

E41: now
let c1 be set ;
let c2 be finite set ;
let c3, c4 be Element of (SubstLatt c1,c2);
deffunc H2( Element of (SubstLatt c1,c2), Element of (SubstLatt c1,c2)) -> Element of the carrier of (SubstLatt c1,c2) = FinJoin (SUB a1),(H1(c1,c2) .: (pseudo_compl c1,c2),((StrongImpl c1,c2) [:] (diff a1),a2));
set c5 = H1(c1,c2) .: (pseudo_compl c1,c2),((StrongImpl c1,c2) [:] (diff c3),c4);
E42: now
let c6 be Element of (SubstLatt c1,c2);
set c7 = (diff c3) . c6;
set c8 = (pseudo_compl c1,c2) . c6;
set c9 = (StrongImpl c1,c2) . ((diff c3) . c6),c4;
assume c6 in SUB c3 ;
then E43: c6 "\/" ((diff c3) . c6) = c3 by Lemma25;
E44: c6 "/\" (((pseudo_compl c1,c2) . c6) "/\" ((StrongImpl c1,c2) . ((diff c3) . c6),c4)) = (c6 "/\" ((pseudo_compl c1,c2) . c6)) "/\" ((StrongImpl c1,c2) . ((diff c3) . c6),c4) by LATTICES:def 7
.= (Bottom (SubstLatt c1,c2)) "/\" ((StrongImpl c1,c2) . ((diff c3) . c6),c4) by Th31
.= Bottom (SubstLatt c1,c2) by LATTICES:40 ;
E45: ((diff c3) . c6) "/\" ((StrongImpl c1,c2) . ((diff c3) . c6),c4) [= c4 by Th32;
(H1(c1,c2) [;] c3,(H1(c1,c2) .: (pseudo_compl c1,c2),((StrongImpl c1,c2) [:] (diff c3),c4))) . c6 = H1(c1,c2) . c3,((H1(c1,c2) .: (pseudo_compl c1,c2),((StrongImpl c1,c2) [:] (diff c3),c4)) . c6) by FUNCOP_1:66
.= c3 "/\" ((H1(c1,c2) .: (pseudo_compl c1,c2),((StrongImpl c1,c2) [:] (diff c3),c4)) . c6) by LATTICES:def 2
.= c3 "/\" (H1(c1,c2) . ((pseudo_compl c1,c2) . c6),(((StrongImpl c1,c2) [:] (diff c3),c4) . c6)) by FUNCOP_1:48
.= c3 "/\" (((pseudo_compl c1,c2) . c6) "/\" (((StrongImpl c1,c2) [:] (diff c3),c4) . c6)) by LATTICES:def 2
.= c3 "/\" (((pseudo_compl c1,c2) . c6) "/\" ((StrongImpl c1,c2) . ((diff c3) . c6),c4)) by FUNCOP_1:60
.= (c6 "/\" (((pseudo_compl c1,c2) . c6) "/\" ((StrongImpl c1,c2) . ((diff c3) . c6),c4))) "\/" (((diff c3) . c6) "/\" (((pseudo_compl c1,c2) . c6) "/\" ((StrongImpl c1,c2) . ((diff c3) . c6),c4))) by E43, LATTICES:def 11
.= ((diff c3) . c6) "/\" (((StrongImpl c1,c2) . ((diff c3) . c6),c4) "/\" ((pseudo_compl c1,c2) . c6)) by E44, LATTICES:39
.= (((diff c3) . c6) "/\" ((StrongImpl c1,c2) . ((diff c3) . c6),c4)) "/\" ((pseudo_compl c1,c2) . c6) by LATTICES:def 7 ;
then (H1(c1,c2) [;] c3,(H1(c1,c2) .: (pseudo_compl c1,c2),((StrongImpl c1,c2) [:] (diff c3),c4))) . c6 [= ((diff c3) . c6) "/\" ((StrongImpl c1,c2) . ((diff c3) . c6),c4) by LATTICES:23;
hence (H1(c1,c2) [;] c3,(H1(c1,c2) .: (pseudo_compl c1,c2),((StrongImpl c1,c2) [:] (diff c3),c4))) . c6 [= c4 by E45, LATTICES:25;
end;
c3 "/\" H2(c3,c4) = FinJoin (SUB c3),(H1(c1,c2) [;] c3,(H1(c1,c2) .: (pseudo_compl c1,c2),((StrongImpl c1,c2) [:] (diff c3),c4))) by LATTICE2:83;
hence c3 "/\" H2(c3,c4) [= c4 by E42, LATTICE2:70;
let c6 be Element of (SubstLatt c1,c2);
reconsider c7 = c4 as Element of SubstitutionSet c1,c2 by SUBSTLAT:def 4;
E43: c4 = FinJoin c7,(Atom c1,c2) by Th24;
then E44: c3 "/\" c4 = FinJoin c7,(H1(c1,c2) [;] c3,(Atom c1,c2)) by LATTICE2:83;
assume E45: c3 "/\" c4 [= c6 ;
now
let c8 be Element of PFuncs c1,c2;
assume E46: c8 in c7 ;
then (H1(c1,c2) [;] c3,(Atom c1,c2)) . c8 [= c6 by E44, E45, LATTICE2:46;
then H1(c1,c2) . c3,((Atom c1,c2) . c8) [= c6 by FUNCOP_1:66;
then E47: c3 "/\" ((Atom c1,c2) . c8) [= c6 by LATTICES:def 2;
reconsider c9 = {c8} as Element of Fin (PFuncs c1,c2) ;
E48: c8 is finite by E46, Th2;
then reconsider c10 = {c8} as Element of SubstitutionSet c1,c2 by Th6;
consider c11 being Element of SubstitutionSet c1,c2 such that
E49: c11 in SUB c3 and
E50: c11 ^ c9 = {} and
E51: for b1 being Element of PFuncs c1,c2 st b1 in (diff c3) . c11 holds
b1 tolerates c8 by E48, Lemma26;
E52: c11 ^ c10 = {} by E50;
reconsider c12 = c11 as Element of (SubstLatt c1,c2) by SUBSTLAT:def 4;
set c13 = (diff c3) . c12;
(diff c3) . c12 [= c3 by Th25;
then ((diff c3) . c12) "/\" ((Atom c1,c2) . c8) [= c3 "/\" ((Atom c1,c2) . c8) by LATTICES:27;
then E53: ((diff c3) . c12) "/\" ((Atom c1,c2) . c8) [= c6 by E47, LATTICES:25;
set c14 = pseudo_compl c1,c2;
set c15 = (StrongImpl c1,c2) [:] (diff c3),c6;
E54: c8 is finite by E46, Th2;
E55: (Atom c1,c2) . c8 [= (pseudo_compl c1,c2) . c12 by E52, Th27;
(Atom c1,c2) . c8 [= (StrongImpl c1,c2) . ((diff c3) . c12),c6 by E51, E53, E54, Th30;
then E56: (Atom c1,c2) . c8 [= ((StrongImpl c1,c2) [:] (diff c3),c6) . c12 by FUNCOP_1:60;
((pseudo_compl c1,c2) . c12) "/\" (((StrongImpl c1,c2) [:] (diff c3),c6) . c12) = H1(c1,c2) . ((pseudo_compl c1,c2) . c12),(((StrongImpl c1,c2) [:] (diff c3),c6) . c12) by LATTICES:def 2
.= (H1(c1,c2) .: (pseudo_compl c1,c2),((StrongImpl c1,c2) [:] (diff c3),c6)) . c12 by FUNCOP_1:48 ;
then (Atom c1,c2) . c8 [= (H1(c1,c2) .: (pseudo_compl c1,c2),((StrongImpl c1,c2) [:] (diff c3),c6)) . c12 by E55, E56, FILTER_0:7;
hence (Atom c1,c2) . c8 [= H2(c3,c6) by E49, LATTICE2:44;
end;
hence c4 [= H2(c3,c6) by E43, LATTICE2:70;
end;

Lemma42: for b1 being set
for b2 being finite set holds SubstLatt b1,b2 is implicative
proof end;

registration
let c1 be set ;
let c2 be finite set ;
cluster SubstLatt a1,a2 -> implicative ;
coherence
SubstLatt c1,c2 is implicative by Lemma42;
end;

theorem Th33: :: HEYTING2:33
for b1 being set
for b2 being finite set
for b3, b4 being Element of (SubstLatt b1,b2) holds b3 => b4 = FinJoin (SUB b3),(the L_meet of (SubstLatt b1,b2) .: (pseudo_compl b1,b2),((StrongImpl b1,b2) [:] (diff b3),b4))
proof end;