:: Algebra of Normal Forms Is a Heyting Algebra
:: by Andrzej Trybulec
::
:: Received January 3, 1991
:: Copyright (c) 1991-2012 Association of Mizar Users


begin

:: Preliminaries
theorem Th1: :: HEYTING1:1
for A, B, C being non empty set
for f being Function of A,B st ( for x being Element of A holds f . x in C ) holds
f is Function of A,C
proofend;

definition
let A be non empty set ;
let B, C be Element of Fin A;
:: original:c=
redefine predB c= C means :: HEYTING1:def 1
 for a being Element of A st a in B holds
a in C;
compatibility
 ( B c= C iff for a being Element of A st a in B holds
a in C )
proofend;
end;

:: deftheorem  defines c= HEYTING1:def_1_:_
 for A being non empty set
for B, C being Element of Fin A holds
( B c= C iff for a being Element of A st a in B holds
a in C );

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

:: deftheorem Def2 defines [ HEYTING1:def_2_:_
 for A being set st not A is empty holds
[A] = A;

theorem :: HEYTING1:2
for A being set
for B being Element of Fin (DISJOINT_PAIRS A) st B = {} holds
mi B = {} by NORMFORM:40, XBOOLE_1:3;

Lm1: now__::_thesis:_for_A_being_set_
for_a_being_Element_of_DISJOINT_PAIRS_A_holds_{a}_is_Element_of_Normal_forms_on_A
let A be set ; ::_thesis: for a being Element of DISJOINT_PAIRS A holds {a} is Element of Normal_forms_on A
let a be Element of DISJOINT_PAIRS A; ::_thesis: {a} is Element of Normal_forms_on A
reconsider B = {.a.} as Element of Fin (DISJOINT_PAIRS A) ;
now__::_thesis:_for_c,_b_being_Element_of_DISJOINT_PAIRS_A_st_c_in_B_&_b_in_B_&_c_c=_b_holds_
c_=_b
let c, b be Element of DISJOINT_PAIRS A; ::_thesis: ( c in B & b in B & c c= b implies c = b )
assume that
A1: c in B and
A2: b in B and
 c c= b ; ::_thesis: c = b
 c = a by A1, TARSKI:def_1;
hence  c = b by A2, TARSKI:def_1; ::_thesis: verum
end;
hence  {a} is Element of Normal_forms_on A by NORMFORM:33; ::_thesis: verum
end;

registration
let A be set ;
cluster non empty for Element of Normal_forms_on A;
existence
 not for b1 being Element of Normal_forms_on A holds b1 is empty
proofend;
end;

definition
let A be set ;
let a be Element of DISJOINT_PAIRS A;
:: original:{
redefine func{a} ->  Element of Normal_forms_on A;
coherence
 {a} is Element of Normal_forms_on A by Lm1;
end;

definition
let A be set ;
let u be Element of (NormForm A);
func @ u ->  Element of Normal_forms_on A equals :: HEYTING1:def 3
u;
coherence
 u is Element of Normal_forms_on A by NORMFORM:def_12;
end;

:: deftheorem  defines @ HEYTING1:def_3_:_
 for A being set
for u being Element of (NormForm A) holds @ u = u;

theorem Th3: :: HEYTING1:3
for A being set
for K being Element of Normal_forms_on A holds mi (K ^ K) = K
proofend;

theorem Th4: :: HEYTING1:4
for A being set
for K being Element of Normal_forms_on A
for X being set st X c= K holds
X in Normal_forms_on A
proofend;

theorem Th5: :: HEYTING1:5
for A being set
for u being Element of (NormForm A)
for X being set st X c= u holds
X is Element of (NormForm A)
proofend;

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

:: deftheorem Def4 defines Atom HEYTING1:def_4_:_
 for A being set
for b2 being Function of (DISJOINT_PAIRS A), the carrier of (NormForm A) holds
( b2 = Atom A iff for a being Element of DISJOINT_PAIRS A holds b2 . a = {a} );

theorem Th6: :: HEYTING1:6
for A being set
for c, a being Element of DISJOINT_PAIRS A st c in (Atom A) . a holds
c = a
proofend;

theorem Th7: :: HEYTING1:7
for A being set
for a being Element of DISJOINT_PAIRS A holds a in (Atom A) . a
proofend;

theorem :: HEYTING1:8
for A being set
for a being Element of DISJOINT_PAIRS A holds (Atom A) . a = (singleton (DISJOINT_PAIRS A)) . a
proofend;

theorem Th9: :: HEYTING1:9
for A being set
for K being Element of Normal_forms_on A holds FinJoin (K,(Atom A)) = FinUnion (K,(singleton (DISJOINT_PAIRS A)))
proofend;

theorem Th10: :: HEYTING1:10
for A being set
for u being Element of (NormForm A) holds u = FinJoin ((@ u),(Atom A))
proofend;

Lm2:  for A being set
for u, v being Element of (NormForm A) st u [= v holds
for x being Element of [:(Fin A),(Fin A):] st x in u holds
ex b being Element of DISJOINT_PAIRS A st
( b in v & b c= x )
proofend;

Lm3:  for A being set
for u, v being Element of (NormForm A) st ( for a being Element of DISJOINT_PAIRS A st a in u holds
ex b being Element of DISJOINT_PAIRS A st
( b in v & b c= a ) ) holds
u [= v
proofend;

definition
let A be set ;
func pair_diff A ->  BinOp of [:(Fin A),(Fin A):] means :Def5: :: HEYTING1:def 5
 for a, b being Element of [:(Fin A),(Fin A):] holds it . (a,b) = a \ b;
existence
 ex b1 being BinOp of [:(Fin A),(Fin A):] st
for a, b being Element of [:(Fin A),(Fin A):] holds b1 . (a,b) = a \ b
proofend;
correctness
uniqueness
for b1, b2 being BinOp of [:(Fin A),(Fin A):] st ( for a, b being Element of [:(Fin A),(Fin A):] holds b1 . (a,b) = a \ b ) & ( for a, b being Element of [:(Fin A),(Fin A):] holds b2 . (a,b) = a \ b ) holds
b1 = b2;
proofend;
end;

:: deftheorem Def5 defines pair_diff HEYTING1:def_5_:_
 for A being set
for b2 being BinOp of [:(Fin A),(Fin A):] holds
( b2 = pair_diff A iff for a, b being Element of [:(Fin A),(Fin A):] holds b2 . (a,b) = a \ b );

definition
let A be set ;
let B be Element of Fin (DISJOINT_PAIRS A);
func - B ->  Element of Fin (DISJOINT_PAIRS A) equals :: HEYTING1:def 6
(DISJOINT_PAIRS A) /\  {  [ {  (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in B )  }  , {  (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in B )  }  ] where g is Element of Funcs ((DISJOINT_PAIRS A),[A]) : for s being Element of DISJOINT_PAIRS A st s in B holds
g . s in (s `1) \/ (s `2)  }  ;
coherence
 (DISJOINT_PAIRS A) /\  {  [ {  (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in B )  }  , {  (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in B )  }  ] where g is Element of Funcs ((DISJOINT_PAIRS A),[A]) : for s being Element of DISJOINT_PAIRS A st s in B holds
g . s in (s `1) \/ (s `2)  }  is Element of Fin (DISJOINT_PAIRS A)
proofend;
correctness
;
let C be Element of Fin (DISJOINT_PAIRS A);
funcB =>> C ->  Element of Fin (DISJOINT_PAIRS A) equals :: HEYTING1:def 7
(DISJOINT_PAIRS A) /\  {  (FinPairUnion (B,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))))) where f is Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : f .: B c= C  }  ;
coherence
 (DISJOINT_PAIRS A) /\  {  (FinPairUnion (B,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))))) where f is Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : f .: B c= C  }  is Element of Fin (DISJOINT_PAIRS A)
proofend;
correctness
;
end;

:: deftheorem  defines - HEYTING1:def_6_:_
 for A being set
for B being Element of Fin (DISJOINT_PAIRS A) holds - B = (DISJOINT_PAIRS A) /\  {  [ {  (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in B )  }  , {  (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in B )  }  ] where g is Element of Funcs ((DISJOINT_PAIRS A),[A]) : for s being Element of DISJOINT_PAIRS A st s in B holds
g . s in (s `1) \/ (s `2)  }  ;

:: deftheorem  defines =>> HEYTING1:def_7_:_
 for A being set
for B, C being Element of Fin (DISJOINT_PAIRS A) holds B =>> C = (DISJOINT_PAIRS A) /\  {  (FinPairUnion (B,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))))) where f is Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : f .: B c= C  }  ;

theorem Th11: :: HEYTING1:11
for A being set
for B being Element of Fin (DISJOINT_PAIRS A)
for c being Element of DISJOINT_PAIRS A st c in - B holds
ex g being Element of Funcs ((DISJOINT_PAIRS A),[A]) st
( ( for s being Element of DISJOINT_PAIRS A st s in B holds
g . s in (s `1) \/ (s `2) ) & c = [ {  (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in B )  }  , {  (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in B )  }  ] )
proofend;

theorem Th12: :: HEYTING1:12
for A being set holds [{},{}] is Element of DISJOINT_PAIRS A
proofend;

theorem Th13: :: HEYTING1:13
for A being set
for K being Element of Normal_forms_on A st K = {} holds
- K = {[{},{}]}
proofend;

theorem Th14: :: HEYTING1:14
for A being set
for K, L being Element of Normal_forms_on A st K = {} & L = {} holds
K =>> L = {[{},{}]}
proofend;

theorem Th15: :: HEYTING1:15
for a being Element of DISJOINT_PAIRS {} holds a = [{},{}]
proofend;

theorem Th16: :: HEYTING1:16
DISJOINT_PAIRS {} = {[{},{}]}
proofend;

Lm4:  Fin (DISJOINT_PAIRS {}) = {{},{[{},{}]}}
proofend;

theorem Th17: :: HEYTING1:17
for A being set holds {[{},{}]} is Element of Normal_forms_on A
proofend;

theorem Th18: :: HEYTING1:18
for A being set
for B, C being Element of Fin (DISJOINT_PAIRS A)
for c being Element of DISJOINT_PAIRS A st c in B =>> C holds
ex f being Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) st
( f .: B c= C & c = FinPairUnion (B,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A))))) )
proofend;

theorem Th19: :: HEYTING1:19
for A being set
for a being Element of DISJOINT_PAIRS A
for K being Element of Normal_forms_on A st K ^ {a} = {} holds
ex b being Element of DISJOINT_PAIRS A st
( b in - K & b c= a )
proofend;

Lm5: now__::_thesis:_for_A_being_set_
for_K_being_Element_of_Normal_forms_on_A
for_b_being_Element_of_DISJOINT_PAIRS_A
for_f_being_Element_of_Funcs_((DISJOINT_PAIRS_A),[:(Fin_A),(Fin_A):])_holds_((pair_diff_A)_.:_(f,(incl_(DISJOINT_PAIRS_A))))_._b_=_(f_._b)_\_b
let A be set ; ::_thesis: for K being Element of Normal_forms_on A
for b being Element of DISJOINT_PAIRS A
for f being Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) holds ((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))) . b = (f . b) \ b
let K be Element of Normal_forms_on A; ::_thesis: for b being Element of DISJOINT_PAIRS A
for f being Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) holds ((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))) . b = (f . b) \ b
let b be Element of DISJOINT_PAIRS A; ::_thesis: for f being Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) holds ((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))) . b = (f . b) \ b
let f be Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]); ::_thesis: ((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))) . b = (f . b) \ b
thus ((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))) . b = (pair_diff A) . ((f . b),((incl (DISJOINT_PAIRS A)) . b)) by FUNCOP_1:37
.= (pair_diff A) . ((f . b),b) by FUNCT_1:18
.= (f . b) \ b by Def5 ; ::_thesis: verum
end;

theorem Th20: :: HEYTING1:20
for A being set
for a being Element of DISJOINT_PAIRS A
for u, v being Element of (NormForm A) st ( for c being Element of DISJOINT_PAIRS A st c in u holds
ex b being Element of DISJOINT_PAIRS A st
( b in v & b c= c \/ a ) ) holds
ex b being Element of DISJOINT_PAIRS A st
( b in (@ u) =>> (@ v) & b c= a )
proofend;

Lm6:  for A being set
for a being Element of DISJOINT_PAIRS A
for u being Element of (NormForm A)
for K being Element of Normal_forms_on A st a in K ^ (K =>> (@ u)) holds
ex b being Element of DISJOINT_PAIRS A st
( b in u & b c= a )
proofend;

theorem Th21: :: HEYTING1:21
for A being set
for K being Element of Normal_forms_on A holds K ^ (- K) = {}
proofend;

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

:: deftheorem Def8 defines pseudo_compl HEYTING1:def_8_:_
 for A being set
for b2 being UnOp of the carrier of (NormForm A) holds
( b2 = pseudo_compl A iff for u being Element of (NormForm A) holds b2 . u = mi (- (@ u)) );

:: deftheorem Def9 defines StrongImpl HEYTING1:def_9_:_
 for A being set
for b2 being BinOp of the carrier of (NormForm A) holds
( b2 = StrongImpl A iff for u, v being Element of (NormForm A) holds b2 . (u,v) = mi ((@ u) =>> (@ v)) );

:: deftheorem  defines SUB HEYTING1:def_10_:_
 for A being set
for u being Element of (NormForm A) holds SUB u = bool u;

:: deftheorem Def11 defines diff HEYTING1:def_11_:_
 for A being set
for u being Element of (NormForm A)
for b3 being UnOp of the carrier of (NormForm A) holds
( b3 = diff u iff for v being Element of (NormForm A) holds b3 . v = u \ v );

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

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

Lm7:  for A being set
for u, v being Element of (NormForm A) st v in SUB u holds
v "\/" ((diff u) . v) = u
proofend;

theorem Th22: :: HEYTING1:22
for A being set
for u, v being Element of (NormForm A) holds (diff u) . v [= u
proofend;

Lm8:  for A being set
for a being Element of DISJOINT_PAIRS A
for u being Element of (NormForm A) ex v being Element of (NormForm A) st
( v in SUB u & (@ v) ^ {a} = {} & ( for b being Element of DISJOINT_PAIRS A st b in (diff u) . v holds
b \/ a in DISJOINT_PAIRS A ) )
proofend;

theorem Th23: :: HEYTING1:23
for A being set
for u being Element of (NormForm A) holds u "/\" ((pseudo_compl A) . u) = Bottom (NormForm A)
proofend;

theorem Th24: :: HEYTING1:24
for A being set
for u, v being Element of (NormForm A) holds u "/\" ((StrongImpl A) . (u,v)) [= v
proofend;

theorem Th25: :: HEYTING1:25
for A being set
for a being Element of DISJOINT_PAIRS A
for u being Element of (NormForm A) st (@ u) ^ {a} = {} holds
(Atom A) . a [= (pseudo_compl A) . u
proofend;

theorem Th26: :: HEYTING1:26
for A being set
for a being Element of DISJOINT_PAIRS A
for u, w being Element of (NormForm A) st ( for b being Element of DISJOINT_PAIRS A st b in u holds
b \/ a in DISJOINT_PAIRS A ) & u "/\" ((Atom A) . a) [= w holds
(Atom A) . a [= (StrongImpl A) . (u,w)
proofend;

Lm9: now__::_thesis:_for_A_being_set_
for_u,_v_being_Element_of_(NormForm_A)_holds_
(_u_"/\"_H3(u,v)_[=_v_&_(_for_w_being_Element_of_(NormForm_A)_st_u_"/\"_v_[=_w_holds_
v_[=_H3(u,w)_)_)
let A be set ; ::_thesis: for u, v being Element of (NormForm A) holds
( u "/\" H3(u,v) [= v & ( for w being Element of (NormForm A) st u "/\" v [= w holds
v [= H3(u,w) ) )
let u, v be Element of (NormForm A); ::_thesis: ( u "/\" H3(u,v) [= v & ( for w being Element of (NormForm A) st u "/\" v [= w holds
v [= H3(u,w) ) )
deffunc H3( Element of (NormForm A), Element of (NormForm A)) ->  Element of the carrier of (NormForm A) = FinJoin ((SUB $1),(H2(A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff $1),$2)))));
set Psi = H2(A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff u),v)));
A1: now__::_thesis:_for_w_being_Element_of_(NormForm_A)_st_w_in_SUB_u_holds_
(H2(A)_[;]_(u,(H2(A)_.:_((pseudo_compl_A),((StrongImpl_A)_[:]_((diff_u),v))))))_._w_[=_v
let w be Element of (NormForm A); ::_thesis: ( w in SUB u implies (H2(A) [;] (u,(H2(A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff u),v)))))) . w [= v )
set u2 = (diff u) . w;
set pc = (pseudo_compl A) . w;
set si = (StrongImpl A) . (((diff u) . w),v);
A2: w "/\" (((pseudo_compl A) . w) "/\" ((StrongImpl A) . (((diff u) . w),v))) = (w "/\" ((pseudo_compl A) . w)) "/\" ((StrongImpl A) . (((diff u) . w),v)) by LATTICES:def_7
.= (Bottom (NormForm A)) "/\" ((StrongImpl A) . (((diff u) . w),v)) by Th23
.= Bottom (NormForm A) ;
assume  w in SUB u ; ::_thesis: (H2(A) [;] (u,(H2(A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff u),v)))))) . w [= v
then A3: w "\/" ((diff u) . w) = u by Lm7;
(H2(A) [;] (u,(H2(A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff u),v)))))) . w = H2(A) . (u,((H2(A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff u),v)))) . w)) by FUNCOP_1:53
.= u "/\" ((H2(A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff u),v)))) . w) by LATTICES:def_2
.= u "/\" (H2(A) . (((pseudo_compl A) . w),(((StrongImpl A) [:] ((diff u),v)) . w))) by FUNCOP_1:37
.= u "/\" (((pseudo_compl A) . w) "/\" (((StrongImpl A) [:] ((diff u),v)) . w)) by LATTICES:def_2
.= u "/\" (((pseudo_compl A) . w) "/\" ((StrongImpl A) . (((diff u) . w),v))) by FUNCOP_1:48
.= (w "/\" (((pseudo_compl A) . w) "/\" ((StrongImpl A) . (((diff u) . w),v)))) "\/" (((diff u) . w) "/\" (((pseudo_compl A) . w) "/\" ((StrongImpl A) . (((diff u) . w),v)))) by A3, LATTICES:def_11
.= ((diff u) . w) "/\" (((StrongImpl A) . (((diff u) . w),v)) "/\" ((pseudo_compl A) . w)) by A2, LATTICES:14
.= (((diff u) . w) "/\" ((StrongImpl A) . (((diff u) . w),v))) "/\" ((pseudo_compl A) . w) by LATTICES:def_7 ;
then A4: (H2(A) [;] (u,(H2(A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff u),v)))))) . w [= ((diff u) . w) "/\" ((StrongImpl A) . (((diff u) . w),v)) by LATTICES:6;
 ((diff u) . w) "/\" ((StrongImpl A) . (((diff u) . w),v)) [= v by Th24;
hence  (H2(A) [;] (u,(H2(A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff u),v)))))) . w [= v by A4, LATTICES:7; ::_thesis: verum
end;
 u "/\" H3(u,v) = FinJoin ((SUB u),(H2(A) [;] (u,(H2(A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff u),v))))))) by LATTICE2:66;
hence  u "/\" H3(u,v) [= v by A1, LATTICE2:54; ::_thesis: for w being Element of (NormForm A) st u "/\" v [= w holds
v [= H3(u,w)
let w be Element of (NormForm A); ::_thesis: ( u "/\" v [= w implies v [= H3(u,w) )
assume A5: u "/\" v [= w ; ::_thesis: v [= H3(u,w)
A6: v = FinJoin ((@ v),(Atom A)) by Th10;
then A7: u "/\" v = FinJoin ((@ v),(H2(A) [;] (u,(Atom A)))) by LATTICE2:66;
now__::_thesis:_for_a_being_Element_of_DISJOINT_PAIRS_A_st_a_in_@_v_holds_
(Atom_A)_._a_[=_H3(u,w)
set pf = pseudo_compl A;
set sf = (StrongImpl A) [:] ((diff u),w);
let a be Element of DISJOINT_PAIRS A; ::_thesis: ( a in @ v implies (Atom A) . a [= H3(u,w) )
assume  a in @ v ; ::_thesis: (Atom A) . a [= H3(u,w)
then  (H2(A) [;] (u,(Atom A))) . a [= w by A7, A5, LATTICE2:31;
then  H2(A) . (u,((Atom A) . a)) [= w by FUNCOP_1:53;
then A8: u "/\" ((Atom A) . a) [= w by LATTICES:def_2;
consider v being Element of (NormForm A) such that
A9: v in SUB u and
A10: (@ v) ^ {a} = {} and
A11: for b being Element of DISJOINT_PAIRS A st b in (diff u) . v holds
b \/ a in DISJOINT_PAIRS A by Lm8;
 ((diff u) . v) "/\" ((Atom A) . a) [= u "/\" ((Atom A) . a) by Th22, LATTICES:9;
then  ((diff u) . v) "/\" ((Atom A) . a) [= w by A8, LATTICES:7;
then  (Atom A) . a [= (StrongImpl A) . (((diff u) . v),w) by A11, Th26;
then A12: (Atom A) . a [= ((StrongImpl A) [:] ((diff u),w)) . v by FUNCOP_1:48;
A13: ((pseudo_compl A) . v) "/\" (((StrongImpl A) [:] ((diff u),w)) . v) = H2(A) . (((pseudo_compl A) . v),(((StrongImpl A) [:] ((diff u),w)) . v)) by LATTICES:def_2
.= (H2(A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff u),w)))) . v by FUNCOP_1:37 ;
 (Atom A) . a [= (pseudo_compl A) . v by A10, Th25;
then  (Atom A) . a [= (H2(A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff u),w)))) . v by A12, A13, FILTER_0:7;
hence  (Atom A) . a [= H3(u,w) by A9, LATTICE2:29; ::_thesis: verum
end;
hence  v [= H3(u,w) by A6, LATTICE2:54; ::_thesis: verum
end;

Lm10:  for A being set holds NormForm A is implicative
proofend;

registration
let A be set ;
cluster NormForm A ->  implicative ;
coherence
 NormForm A is implicative by Lm10;
end;

theorem Th27: :: HEYTING1:27
for A being set
for u, v being Element of (NormForm A) holds u => v = FinJoin ((SUB u),( the L_meet of (NormForm A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff u),v)))))
proofend;

theorem :: HEYTING1:28
for A being set holds Top (NormForm A) = {[{},{}]}
proofend;