:: HEYTING1 semantic presentation

theorem Th1: :: HEYTING1:1
for b1, b2, b3 being non empty set
for b4 being Function of b1,b2 st ( for b5 being Element of b1 holds b4 . b5 in b3 ) holds
b4 is Function of b1,b3
proof end;

definition
let c1 be non empty set ;
let c2, c3 be Element of Fin c1;
redefine pred c= as c2 c= c3 means :: HEYTING1:def 1
for b1 being Element of a1 st b1 in a2 holds
b1 in a3;
compatibility
( c2 c= c3 iff for b1 being Element of c1 st b1 in c2 holds
b1 in c3 )
proof end;
end;

:: deftheorem Def1 defines c= HEYTING1:def 1 :
for b1 being non empty set
for b2, b3 being Element of Fin b1 holds
( b2 c= b3 iff for b4 being Element of b1 st b4 in b2 holds
b4 in b3 );

definition
let c1 be set ;
assume E2: not c1 is empty ;
func [c1] -> non empty set equals :Def2: :: HEYTING1:def 2
a1;
correctness
coherence
c1 is non empty set ;
by E2;
end;

:: deftheorem Def2 defines [ HEYTING1:def 2 :
for b1 being set st not b1 is empty holds
[b1] = b1;

theorem Th2: :: HEYTING1:2
canceled;

theorem Th3: :: HEYTING1:3
for b1 being set
for b2 being Element of Fin (DISJOINT_PAIRS b1) st b2 = {} holds
mi b2 = {}
proof end;

E4: now
let c1 be set ;
let c2 be Element of DISJOINT_PAIRS c1;
reconsider c3 = {c2} as Element of Fin (DISJOINT_PAIRS c1) ;
now
let c4, c5 be Element of DISJOINT_PAIRS c1;
assume that
E5: ( c4 in c3 & c5 in c3 ) and
c4 c= c5 ;
( c4 = c2 & c5 = c2 ) by E5, TARSKI:def 1;
hence c4 = c5 ;
end;
hence {c2} is Element of Normal_forms_on c1 by NORMFORM:53;
end;

registration
let c1 be set ;
cluster non empty Element of Normal_forms_on a1;
existence
not for b1 being Element of Normal_forms_on c1 holds b1 is empty
proof end;
end;

definition
let c1 be set ;
let c2 be Element of DISJOINT_PAIRS c1;
redefine func { as {c2} -> Element of Normal_forms_on a1;
coherence
{c2} is Element of Normal_forms_on c1 by Lemma4;
end;

definition
let c1 be set ;
let c2 be Element of (NormForm c1);
func @ c2 -> Element of Normal_forms_on a1 equals :: HEYTING1:def 3
a2;
coherence
c2 is Element of Normal_forms_on c1 by NORMFORM:def 14;
end;

:: deftheorem Def3 defines @ HEYTING1:def 3 :
for b1 being set
for b2 being Element of (NormForm b1) holds @ b2 = b2;

Lemma5: for b1 being set
for b2, b3 being Element of (NormForm b1) holds mi ((@ b2) ^ (@ b3)) = the L_meet of (NormForm b1) . b2,b3
by NORMFORM:def 14;

Lemma6: for b1 being set
for b2, b3 being Element of (NormForm b1) holds mi ((@ b2) \/ (@ b3)) = the L_join of (NormForm b1) . b2,b3
by NORMFORM:def 14;

theorem Th4: :: HEYTING1:4
canceled;

theorem Th5: :: HEYTING1:5
canceled;

theorem Th6: :: HEYTING1:6
canceled;

theorem Th7: :: HEYTING1:7
for b1 being set
for b2 being Element of Normal_forms_on b1 holds mi (b2 ^ b2) = b2
proof end;

theorem Th8: :: HEYTING1:8
for b1 being set
for b2 being Element of Normal_forms_on b1
for b3 being set st b3 c= b2 holds
b3 in Normal_forms_on b1
proof end;

theorem Th9: :: HEYTING1:9
canceled;

theorem Th10: :: HEYTING1:10
for b1 being set
for b2 being Element of (NormForm b1)
for b3 being set st b3 c= b2 holds
b3 is Element of (NormForm b1)
proof end;

definition
let c1 be set ;
func Atom c1 -> Function of DISJOINT_PAIRS a1,the carrier of (NormForm a1) means :Def4: :: HEYTING1:def 4
for b1 being Element of DISJOINT_PAIRS a1 holds a2 . b1 = {b1};
existence
ex b1 being Function of DISJOINT_PAIRS c1,the carrier of (NormForm c1) st
for b2 being Element of DISJOINT_PAIRS c1 holds b1 . b2 = {b2}
proof end;
uniqueness
for b1, b2 being Function of DISJOINT_PAIRS c1,the carrier of (NormForm c1) st ( for b3 being Element of DISJOINT_PAIRS c1 holds b1 . b3 = {b3} ) & ( for b3 being Element of DISJOINT_PAIRS c1 holds b2 . b3 = {b3} ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines Atom HEYTING1:def 4 :
for b1 being set
for b2 being Function of DISJOINT_PAIRS b1,the carrier of (NormForm b1) holds
( b2 = Atom b1 iff for b3 being Element of DISJOINT_PAIRS b1 holds b2 . b3 = {b3} );

theorem Th11: :: HEYTING1:11
for b1 being set
for b2, b3 being Element of DISJOINT_PAIRS b1 st b2 in (Atom b1) . b3 holds
b2 = b3
proof end;

theorem Th12: :: HEYTING1:12
for b1 being set
for b2 being Element of DISJOINT_PAIRS b1 holds b2 in (Atom b1) . b2
proof end;

theorem Th13: :: HEYTING1:13
for b1 being set
for b2 being Element of DISJOINT_PAIRS b1 holds (Atom b1) . b2 = (singleton (DISJOINT_PAIRS b1)) . b2
proof end;

theorem Th14: :: HEYTING1:14
for b1 being set
for b2 being Element of Normal_forms_on b1 holds FinJoin b2,(Atom b1) = FinUnion b2,(singleton (DISJOINT_PAIRS b1))
proof end;

theorem Th15: :: HEYTING1:15
for b1 being set
for b2 being Element of (NormForm b1) holds b2 = FinJoin (@ b2),(Atom b1)
proof end;

Lemma15: for b1 being set
for b2, b3 being Element of (NormForm b1) st b2 [= b3 holds
for b4 being Element of [:(Fin b1),(Fin b1):] st b4 in b2 holds
ex b5 being Element of DISJOINT_PAIRS b1 st
( b5 in b3 & b5 c= b4 )
proof end;

Lemma16: for b1 being set
for b2, b3 being Element of (NormForm b1) st ( for b4 being Element of DISJOINT_PAIRS b1 st b4 in b2 holds
ex b5 being Element of DISJOINT_PAIRS b1 st
( b5 in b3 & b5 c= b4 ) ) holds
b2 [= b3
proof end;

definition
let c1 be set ;
func pair_diff c1 -> BinOp of [:(Fin a1),(Fin a1):] means :Def5: :: HEYTING1:def 5
for b1, b2 being Element of [:(Fin a1),(Fin a1):] holds a2 . b1,b2 = b1 \ b2;
existence
ex b1 being BinOp of [:(Fin c1),(Fin c1):] st
for b2, b3 being Element of [:(Fin c1),(Fin c1):] holds b1 . b2,b3 = b2 \ b3
proof end;
correctness
uniqueness
for b1, b2 being BinOp of [:(Fin c1),(Fin c1):] st ( for b3, b4 being Element of [:(Fin c1),(Fin c1):] holds b1 . b3,b4 = b3 \ b4 ) & ( for b3, b4 being Element of [:(Fin c1),(Fin c1):] holds b2 . b3,b4 = b3 \ b4 ) holds
b1 = b2;
proof end;
end;

:: deftheorem Def5 defines pair_diff HEYTING1:def 5 :
for b1 being set
for b2 being BinOp of [:(Fin b1),(Fin b1):] holds
( b2 = pair_diff b1 iff for b3, b4 being Element of [:(Fin b1),(Fin b1):] holds b2 . b3,b4 = b3 \ b4 );

definition
let c1 be set ;
let c2 be Element of Fin (DISJOINT_PAIRS c1);
func - c2 -> Element of Fin (DISJOINT_PAIRS a1) equals :: HEYTING1:def 6
(DISJOINT_PAIRS a1) /\ { [{ (b1 . b2) where B is Element of DISJOINT_PAIRS a1 : ( b1 . b2 in b2 `2 & b2 in a2 ) } ,{ (b1 . b2) where B is Element of DISJOINT_PAIRS a1 : ( b1 . b2 in b2 `1 & b2 in a2 ) } ] where B is Element of Funcs (DISJOINT_PAIRS a1),[a1] : for b1 being Element of DISJOINT_PAIRS a1 st b2 in a2 holds
b1 . b2 in (b2 `1 ) \/ (b2 `2 ) } ;
coherence
(DISJOINT_PAIRS c1) /\ { [{ (b1 . b2) where B is Element of DISJOINT_PAIRS c1 : ( b1 . b2 in b2 `2 & b2 in c2 ) } ,{ (b1 . b2) where B is Element of DISJOINT_PAIRS c1 : ( b1 . b2 in b2 `1 & b2 in c2 ) } ] where B is Element of Funcs (DISJOINT_PAIRS c1),[c1] : for b1 being Element of DISJOINT_PAIRS c1 st b2 in c2 holds
b1 . b2 in (b2 `1 ) \/ (b2 `2 ) } is Element of Fin (DISJOINT_PAIRS c1)
proof end;
correctness
;
let c3 be Element of Fin (DISJOINT_PAIRS c1);
func c2 =>> c3 -> Element of Fin (DISJOINT_PAIRS a1) equals :: HEYTING1:def 7
(DISJOINT_PAIRS a1) /\ { (FinPairUnion a2,((pair_diff a1) .: b1,(incl (DISJOINT_PAIRS a1)))) where B is Element of Funcs (DISJOINT_PAIRS a1),[:(Fin a1),(Fin a1):] : b1 .: a2 c= a3 } ;
coherence
(DISJOINT_PAIRS c1) /\ { (FinPairUnion c2,((pair_diff c1) .: b1,(incl (DISJOINT_PAIRS c1)))) where B is Element of Funcs (DISJOINT_PAIRS c1),[:(Fin c1),(Fin c1):] : b1 .: c2 c= c3 } is Element of Fin (DISJOINT_PAIRS c1)
proof end;
correctness
;
end;

:: deftheorem Def6 defines - HEYTING1:def 6 :
for b1 being set
for b2 being Element of Fin (DISJOINT_PAIRS b1) holds - b2 = (DISJOINT_PAIRS b1) /\ { [{ (b3 . b4) where B is Element of DISJOINT_PAIRS b1 : ( b3 . b4 in b4 `2 & b4 in b2 ) } ,{ (b3 . b4) where B is Element of DISJOINT_PAIRS b1 : ( b3 . b4 in b4 `1 & b4 in b2 ) } ] where B is Element of Funcs (DISJOINT_PAIRS b1),[b1] : for b1 being Element of DISJOINT_PAIRS b1 st b4 in b2 holds
b3 . b4 in (b4 `1 ) \/ (b4 `2 ) } ;

:: deftheorem Def7 defines =>> HEYTING1:def 7 :
for b1 being set
for b2, b3 being Element of Fin (DISJOINT_PAIRS b1) holds b2 =>> b3 = (DISJOINT_PAIRS b1) /\ { (FinPairUnion b2,((pair_diff b1) .: b4,(incl (DISJOINT_PAIRS b1)))) where B is Element of Funcs (DISJOINT_PAIRS b1),[:(Fin b1),(Fin b1):] : b4 .: b2 c= b3 } ;

theorem Th16: :: HEYTING1:16
for b1 being set
for b2 being Element of Fin (DISJOINT_PAIRS b1)
for b3 being Element of DISJOINT_PAIRS b1 st b3 in - b2 holds
ex b4 being Element of Funcs (DISJOINT_PAIRS b1),[b1] st
( ( for b5 being Element of DISJOINT_PAIRS b1 st b5 in b2 holds
b4 . b5 in (b5 `1 ) \/ (b5 `2 ) ) & b3 = [{ (b4 . b5) where B is Element of DISJOINT_PAIRS b1 : ( b4 . b5 in b5 `2 & b5 in b2 ) } ,{ (b4 . b5) where B is Element of DISJOINT_PAIRS b1 : ( b4 . b5 in b5 `1 & b5 in b2 ) } ] )
proof end;

theorem Th17: :: HEYTING1:17
for b1 being set holds [{} ,{} ] is Element of DISJOINT_PAIRS b1
proof end;

theorem Th18: :: HEYTING1:18
for b1 being set
for b2 being Element of Normal_forms_on b1 st b2 = {} holds
- b2 = {[{} ,{} ]}
proof end;

theorem Th19: :: HEYTING1:19
for b1 being set
for b2, b3 being Element of Normal_forms_on b1 st b2 = {} & b3 = {} holds
b2 =>> b3 = {[{} ,{} ]}
proof end;

theorem Th20: :: HEYTING1:20
for b1 being Element of DISJOINT_PAIRS {} holds b1 = [{} ,{} ]
proof end;

theorem Th21: :: HEYTING1:21
DISJOINT_PAIRS {} = {[{} ,{} ]}
proof end;

Lemma24: Fin (DISJOINT_PAIRS {} ) = {{} ,{[{} ,{} ]}}
proof end;

theorem Th22: :: HEYTING1:22
for b1 being set holds {[{} ,{} ]} is Element of Normal_forms_on b1
proof end;

theorem Th23: :: HEYTING1:23
for b1 being set
for b2, b3 being Element of Fin (DISJOINT_PAIRS b1)
for b4 being Element of DISJOINT_PAIRS b1 st b4 in b2 =>> b3 holds
ex b5 being Element of Funcs (DISJOINT_PAIRS b1),[:(Fin b1),(Fin b1):] st
( b5 .: b2 c= b3 & b4 = FinPairUnion b2,((pair_diff b1) .: b5,(incl (DISJOINT_PAIRS b1))) )
proof end;

theorem Th24: :: HEYTING1:24
for b1 being set
for b2 being Element of DISJOINT_PAIRS b1
for b3 being Element of Normal_forms_on b1 st b3 ^ {b2} = {} holds
ex b4 being Element of DISJOINT_PAIRS b1 st
( b4 in - b3 & b4 c= b2 )
proof end;

E28: now
let c1 be set ;
let c2 be Element of Normal_forms_on c1;
let c3 be Element of DISJOINT_PAIRS c1;
let c4 be Element of Funcs (DISJOINT_PAIRS c1),[:(Fin c1),(Fin c1):];
thus ((pair_diff c1) .: c4,(incl (DISJOINT_PAIRS c1))) . c3 = (pair_diff c1) . (c4 . c3),((incl (DISJOINT_PAIRS c1)) . c3) by FUNCOP_1:48
.= (pair_diff c1) . (c4 . c3),c3 by FUNCT_1:35
.= (c4 . c3) \ c3 by Def5 ;
end;

theorem Th25: :: HEYTING1:25
for b1 being set
for b2 being Element of DISJOINT_PAIRS b1
for b3, b4 being Element of (NormForm b1) st ( for b5 being Element of DISJOINT_PAIRS b1 st b5 in b3 holds
b5 \/ b2 in DISJOINT_PAIRS b1 ) & ( for b5 being Element of DISJOINT_PAIRS b1 st b5 in b3 holds
ex b6 being Element of DISJOINT_PAIRS b1 st
( b6 in b4 & b6 c= b5 \/ b2 ) ) holds
ex b5 being Element of DISJOINT_PAIRS b1 st
( b5 in (@ b3) =>> (@ b4) & b5 c= b2 )
proof end;

Lemma30: for b1 being set
for b2 being Element of DISJOINT_PAIRS b1
for b3 being Element of (NormForm b1)
for b4 being Element of Normal_forms_on b1 st b2 in b4 ^ (b4 =>> (@ b3)) holds
ex b5 being Element of DISJOINT_PAIRS b1 st
( b5 in b3 & b5 c= b2 )
proof end;

theorem Th26: :: HEYTING1:26
for b1 being set
for b2 being Element of Normal_forms_on b1 holds b2 ^ (- b2) = {}
proof end;

definition
let c1 be set ;
func pseudo_compl c1 -> UnOp of the carrier of (NormForm a1) means :Def8: :: HEYTING1:def 8
for b1 being Element of (NormForm a1) holds a2 . b1 = mi (- (@ b1));
existence
ex b1 being UnOp of the carrier of (NormForm c1) st
for b2 being Element of (NormForm c1) holds b1 . b2 = mi (- (@ b2))
proof end;
correctness
uniqueness
for b1, b2 being UnOp of the carrier of (NormForm c1) st ( for b3 being Element of (NormForm c1) holds b1 . b3 = mi (- (@ b3)) ) & ( for b3 being Element of (NormForm c1) holds b2 . b3 = mi (- (@ b3)) ) holds
b1 = b2;
proof end;
func StrongImpl c1 -> BinOp of the carrier of (NormForm a1) means :Def9: :: HEYTING1:def 9
for b1, b2 being Element of (NormForm a1) holds a2 . b1,b2 = mi ((@ b1) =>> (@ b2));
existence
ex b1 being BinOp of the carrier of (NormForm c1) st
for b2, b3 being Element of (NormForm c1) holds b1 . b2,b3 = mi ((@ b2) =>> (@ b3))
proof end;
correctness
uniqueness
for b1, b2 being BinOp of the carrier of (NormForm c1) st ( for b3, b4 being Element of (NormForm c1) holds b1 . b3,b4 = mi ((@ b3) =>> (@ b4)) ) & ( for b3, b4 being Element of (NormForm c1) holds b2 . b3,b4 = mi ((@ b3) =>> (@ b4)) ) holds
b1 = b2;
proof end;
let c2 be Element of (NormForm c1);
func SUB c2 -> Element of Fin the carrier of (NormForm a1) equals :: HEYTING1:def 10
 bool a2;
coherence
bool c2 is Element of Fin the carrier of (NormForm c1)
proof end;
correctness
;
func diff c2 -> UnOp of the carrier of (NormForm a1) means :Def11: :: HEYTING1:def 11
for b1 being Element of (NormForm a1) holds a3 . b1 = a2 \ b1;
existence
ex b1 being UnOp of the carrier of (NormForm c1) st
for b2 being Element of (NormForm c1) holds b1 . b2 = c2 \ b2
proof end;
correctness
uniqueness
for b1, b2 being UnOp of the carrier of (NormForm c1) st ( for b3 being Element of (NormForm c1) holds b1 . b3 = c2 \ b3 ) & ( for b3 being Element of (NormForm c1) holds b2 . b3 = c2 \ b3 ) holds
b1 = b2;
proof end;
end;

:: deftheorem Def8 defines pseudo_compl HEYTING1:def 8 :
for b1 being set
for b2 being UnOp of the carrier of (NormForm b1) holds
( b2 = pseudo_compl b1 iff for b3 being Element of (NormForm b1) holds b2 . b3 = mi (- (@ b3)) );

:: deftheorem Def9 defines StrongImpl HEYTING1:def 9 :
for b1 being set
for b2 being BinOp of the carrier of (NormForm b1) holds
( b2 = StrongImpl b1 iff for b3, b4 being Element of (NormForm b1) holds b2 . b3,b4 = mi ((@ b3) =>> (@ b4)) );

:: deftheorem Def10 defines SUB HEYTING1:def 10 :
for b1 being set
for b2 being Element of (NormForm b1) holds SUB b2 = bool b2;

:: deftheorem Def11 defines diff HEYTING1:def 11 :
for b1 being set
for b2 being Element of (NormForm b1)
for b3 being UnOp of the carrier of (NormForm b1) holds
( b3 = diff b2 iff for b4 being Element of (NormForm b1) holds b3 . b4 = b2 \ b4 );

deffunc H1( set ) -> M5([:the carrier of (NormForm a1),the carrier of (NormForm a1):],the carrier of (NormForm a1)) = the L_join of (NormForm a1);

deffunc H2( set ) -> M5([:the carrier of (NormForm a1),the carrier of (NormForm a1):],the carrier of (NormForm a1)) = the L_meet of (NormForm a1);

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

theorem Th27: :: HEYTING1:27
for b1 being set
for b2, b3 being Element of (NormForm b1) holds (diff b2) . b3 [= b2
proof end;

Lemma37: for b1 being set
for b2 being Element of DISJOINT_PAIRS b1
for b3 being Element of (NormForm b1) ex b4 being Element of (NormForm b1) st
( b4 in SUB b3 & (@ b4) ^ {b2} = {} & ( for b5 being Element of DISJOINT_PAIRS b1 st b5 in (diff b3) . b4 holds
b5 \/ b2 in DISJOINT_PAIRS b1 ) )
proof end;

theorem Th28: :: HEYTING1:28
for b1 being set
for b2 being Element of (NormForm b1) holds b2 "/\" ((pseudo_compl b1) . b2) = Bottom (NormForm b1)
proof end;

theorem Th29: :: HEYTING1:29
for b1 being set
for b2, b3 being Element of (NormForm b1) holds b2 "/\" ((StrongImpl b1) . b2,b3) [= b3
proof end;

theorem Th30: :: HEYTING1:30
for b1 being set
for b2 being Element of DISJOINT_PAIRS b1
for b3 being Element of (NormForm b1) st (@ b3) ^ {b2} = {} holds
(Atom b1) . b2 [= (pseudo_compl b1) . b3
proof end;

theorem Th31: :: HEYTING1:31
for b1 being set
for b2 being Element of DISJOINT_PAIRS b1
for b3, b4 being Element of (NormForm b1) st ( for b5 being Element of DISJOINT_PAIRS b1 st b5 in b3 holds
b5 \/ b2 in DISJOINT_PAIRS b1 ) & b3 "/\" ((Atom b1) . b2) [= b4 holds
(Atom b1) . b2 [= (StrongImpl b1) . b3,b4
proof end;

E42: now
let c1 be set ;
let c2, c3 be Element of (NormForm c1);
deffunc H3( Element of (NormForm c1), Element of (NormForm c1)) -> Element of the carrier of (NormForm c1) = FinJoin (SUB a1),(H2(c1) .: (pseudo_compl c1),((StrongImpl c1) [:] (diff a1),a2));
set c4 = H2(c1) .: (pseudo_compl c1),((StrongImpl c1) [:] (diff c2),c3);
E43: now
let c5 be Element of (NormForm c1);
set c6 = (diff c2) . c5;
set c7 = (pseudo_compl c1) . c5;
set c8 = (StrongImpl c1) . ((diff c2) . c5),c3;
assume c5 in SUB c2 ;
then E44: c5 "\/" ((diff c2) . c5) = c2 by Lemma35;
E45: c5 "/\" (((pseudo_compl c1) . c5) "/\" ((StrongImpl c1) . ((diff c2) . c5),c3)) = (c5 "/\" ((pseudo_compl c1) . c5)) "/\" ((StrongImpl c1) . ((diff c2) . c5),c3) by LATTICES:def 7
.= (Bottom (NormForm c1)) "/\" ((StrongImpl c1) . ((diff c2) . c5),c3) by Th28
.= Bottom (NormForm c1) by LATTICES:40 ;
E46: ((diff c2) . c5) "/\" ((StrongImpl c1) . ((diff c2) . c5),c3) [= c3 by Th29;
(H2(c1) [;] c2,(H2(c1) .: (pseudo_compl c1),((StrongImpl c1) [:] (diff c2),c3))) . c5 = H2(c1) . c2,((H2(c1) .: (pseudo_compl c1),((StrongImpl c1) [:] (diff c2),c3)) . c5) by FUNCOP_1:66
.= c2 "/\" ((H2(c1) .: (pseudo_compl c1),((StrongImpl c1) [:] (diff c2),c3)) . c5) by LATTICES:def 2
.= c2 "/\" (H2(c1) . ((pseudo_compl c1) . c5),(((StrongImpl c1) [:] (diff c2),c3) . c5)) by FUNCOP_1:48
.= c2 "/\" (((pseudo_compl c1) . c5) "/\" (((StrongImpl c1) [:] (diff c2),c3) . c5)) by LATTICES:def 2
.= c2 "/\" (((pseudo_compl c1) . c5) "/\" ((StrongImpl c1) . ((diff c2) . c5),c3)) by FUNCOP_1:60
.= (c5 "/\" (((pseudo_compl c1) . c5) "/\" ((StrongImpl c1) . ((diff c2) . c5),c3))) "\/" (((diff c2) . c5) "/\" (((pseudo_compl c1) . c5) "/\" ((StrongImpl c1) . ((diff c2) . c5),c3))) by E44, LATTICES:def 11
.= ((diff c2) . c5) "/\" (((StrongImpl c1) . ((diff c2) . c5),c3) "/\" ((pseudo_compl c1) . c5)) by E45, LATTICES:39
.= (((diff c2) . c5) "/\" ((StrongImpl c1) . ((diff c2) . c5),c3)) "/\" ((pseudo_compl c1) . c5) by LATTICES:def 7 ;
then (H2(c1) [;] c2,(H2(c1) .: (pseudo_compl c1),((StrongImpl c1) [:] (diff c2),c3))) . c5 [= ((diff c2) . c5) "/\" ((StrongImpl c1) . ((diff c2) . c5),c3) by LATTICES:23;
hence (H2(c1) [;] c2,(H2(c1) .: (pseudo_compl c1),((StrongImpl c1) [:] (diff c2),c3))) . c5 [= c3 by E46, LATTICES:25;
end;
c2 "/\" H3(c2,c3) = FinJoin (SUB c2),(H2(c1) [;] c2,(H2(c1) .: (pseudo_compl c1),((StrongImpl c1) [:] (diff c2),c3))) by LATTICE2:83;
hence c2 "/\" H3(c2,c3) [= c3 by E43, LATTICE2:70;
let c5 be Element of (NormForm c1);
E44: c3 = FinJoin (@ c3),(Atom c1) by Th15;
then E45: c2 "/\" c3 = FinJoin (@ c3),(H2(c1) [;] c2,(Atom c1)) by LATTICE2:83;
assume E46: c2 "/\" c3 [= c5 ;
now
let c6 be Element of DISJOINT_PAIRS c1;
assume c6 in @ c3 ;
then (H2(c1) [;] c2,(Atom c1)) . c6 [= c5 by E45, E46, LATTICE2:46;
then H2(c1) . c2,((Atom c1) . c6) [= c5 by FUNCOP_1:66;
then E47: c2 "/\" ((Atom c1) . c6) [= c5 by LATTICES:def 2;
consider c7 being Element of (NormForm c1) such that
E48: c7 in SUB c2 and
E49: (@ c7) ^ {c6} = {} and
E50: for b1 being Element of DISJOINT_PAIRS c1 st b1 in (diff c2) . c7 holds
b1 \/ c6 in DISJOINT_PAIRS c1 by Lemma37;
(diff c2) . c7 [= c2 by Th27;
then ((diff c2) . c7) "/\" ((Atom c1) . c6) [= c2 "/\" ((Atom c1) . c6) by LATTICES:27;
then E51: ((diff c2) . c7) "/\" ((Atom c1) . c6) [= c5 by E47, LATTICES:25;
set c8 = pseudo_compl c1;
set c9 = (StrongImpl c1) [:] (diff c2),c5;
E52: (Atom c1) . c6 [= (pseudo_compl c1) . c7 by E49, Th30;
(Atom c1) . c6 [= (StrongImpl c1) . ((diff c2) . c7),c5 by E50, E51, Th31;
then E53: (Atom c1) . c6 [= ((StrongImpl c1) [:] (diff c2),c5) . c7 by FUNCOP_1:60;
((pseudo_compl c1) . c7) "/\" (((StrongImpl c1) [:] (diff c2),c5) . c7) = H2(c1) . ((pseudo_compl c1) . c7),(((StrongImpl c1) [:] (diff c2),c5) . c7) by LATTICES:def 2
.= (H2(c1) .: (pseudo_compl c1),((StrongImpl c1) [:] (diff c2),c5)) . c7 by FUNCOP_1:48 ;
then (Atom c1) . c6 [= (H2(c1) .: (pseudo_compl c1),((StrongImpl c1) [:] (diff c2),c5)) . c7 by E52, E53, FILTER_0:7;
hence (Atom c1) . c6 [= H3(c2,c5) by E48, LATTICE2:44;
end;
hence c3 [= H3(c2,c5) by E44, LATTICE2:70;
end;

Lemma43: for b1 being set holds NormForm b1 is implicative
proof end;

registration
let c1 be set ;
cluster NormForm a1 -> implicative ;
coherence
NormForm c1 is implicative by Lemma43;
end;

theorem Th32: :: HEYTING1:32
canceled;

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

theorem Th34: :: HEYTING1:34
for b1 being set holds Top (NormForm b1) = {[{} ,{} ]}
proof end;