:: Lattice of Substitutions Is a Heyting Algebra
:: by Adam Grabowski
::
:: Received December 31, 1998
:: Copyright (c) 1998-2021 Association of Mizar Users

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 end;

Lm1: for A, B, C being set st A = B \/ C & A c= B holds
A = B
by XBOOLE_1:7;

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 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 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 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 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 object holds
( x in it iff ex f being finite Function st
( f in A & x in dom f ) );

existence
ex b₁ being set st
for x being object holds
( x in b₁ iff ex f being finite Function st
( f in A & x in dom f ) )

proof end;

uniqueness
for b₁, b₂ being set st ( for x being object holds
( x in b₁ iff ex f being finite Function st
( f in A & x in dom f ) ) ) & ( for x being object holds
( x in b₂ iff ex f being finite Function st
( f in A & x in dom f ) ) ) holds
b₁ = b₂

proof 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 b₄ being set holds
( b₄ = Involved A iff for x being object holds
( x in b₄ 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 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 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 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 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 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 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 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 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 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 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 end;

definition

let V be set ;
let C be finite set ;
let A, B be Element of Fin (PFuncs (V,C));

func A =>> 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 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 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 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 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 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 end;

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 b₁ 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
b₁ . u = mi (- u9)

proof end;

correctness
uniqueness
for b₁, b₂ 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
b₁ . u = mi (- u9) ) & ( for u being Element of (SubstLatt (V,C))
for u9 being Element of SubstitutionSet (V,C) st u9 = u holds
b₂ . u = mi (- u9) ) holds
b₁ = b₂;

proof 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 b₁ 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
b₁ . (u,v) = mi (u9 =>> v9)

proof end;

correctness
uniqueness
for b₁, b₂ 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
b₁ . (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
b₂ . (u,v) = mi (u9 =>> v9) ) holds
b₁ = b₂;

proof 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 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 b₁ being UnOp of the carrier of (SubstLatt (V,C)) st
for v being Element of (SubstLatt (V,C)) holds b₁ . v = u \ v

proof end;

correctness
uniqueness
for b₁, b₂ being UnOp of the carrier of (SubstLatt (V,C)) st ( for v being Element of (SubstLatt (V,C)) holds b₁ . v = u \ v ) & ( for v being Element of (SubstLatt (V,C)) holds b₂ . v = u \ v ) holds
b₁ = b₂;

proof end;

end;

:: deftheorem Def4 defines pseudo_compl HEYTING2:def 4 :
for V being set
for C being finite set
for b₃ being UnOp of the carrier of (SubstLatt (V,C)) holds
( b₃ = 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
b₃ . u = mi (- u9) );

:: deftheorem Def5 defines StrongImpl HEYTING2:def 5 :
for V being set
for C being finite set
for b₃ being BinOp of the carrier of (SubstLatt (V,C)) holds
( b₃ = 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
b₃ . (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 b₄ being UnOp of the carrier of (SubstLatt (V,C)) holds
( b₄ = diff u iff for v being Element of (SubstLatt (V,C)) holds b₄ . v = u \ v );

Lm5: for V being set
for C being finite set
for u, v being Element of (SubstLatt (V,C)) st v in SUB u holds
v "\/" ((diff u) . v) = u

proof 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 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 b₁ being Function of (PFuncs (V,C)), the carrier of (SubstLatt (V,C)) st
for a being Element of PFuncs (V,C) holds b₁ . a = mi {.a.}

proof end;

correctness
uniqueness
for b₁, b₂ being Function of (PFuncs (V,C)), the carrier of (SubstLatt (V,C)) st ( for a being Element of PFuncs (V,C) holds b₁ . a = mi {.a.} ) & ( for a being Element of PFuncs (V,C) holds b₂ . a = mi {.a.} ) holds
b₁ = b₂;

proof end;

end;

:: deftheorem Def8 defines Atom HEYTING2:def 8 :
for V being set
for C being finite set
for b₃ being Function of (PFuncs (V,C)), the carrier of (SubstLatt (V,C)) holds
( b₃ = Atom (V,C) iff for a being Element of PFuncs (V,C) holds b₃ . 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 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 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 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 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 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 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 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 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 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 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 end;

deffunc H₁( 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 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 end;

Lm10: now :: thesis: for V being set
for C being finite set
for u, v being Element of (SubstLatt (V,C)) holds
( u "/\" H₂(u,v) [= v & ( for w being Element of (SubstLatt (V,C)) st u "/\" v [= w holds
v [= H₂(u,w) ) )

let V be set ; :: thesis: for C being finite set
for u, v being Element of (SubstLatt (V,C)) holds
( u "/\" H₂(u,v) [= v & ( for w being Element of (SubstLatt (V,C)) st u "/\" v [= w holds
v [= H₂(u,w) ) )
let C be finite set ; :: thesis: for u, v being Element of (SubstLatt (V,C)) holds
( u "/\" H₂(u,v) [= v & ( for w being Element of (SubstLatt (V,C)) st u "/\" v [= w holds
v [= H₂(u,w) ) )
let u, v be Element of (SubstLatt (V,C)); :: thesis: ( u "/\" H₂(u,v) [= v & ( for w being Element of (SubstLatt (V,C)) st u "/\" v [= w holds
v [= H₂(u,w) ) )
deffunc H₂( Element of (SubstLatt (V,C)), Element of (SubstLatt (V,C))) -> Element of the carrier of (SubstLatt (V,C)) = FinJoin ((SUB $1),(H₁(V,C) .: ((pseudo_compl (V,C)),((StrongImpl (V,C)) [:] ((diff $1),$2)))));
set Psi = H₁(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
(H₁(V,C) [;] (u,(H₁(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 (H₁(V,C) [;] (u,(H₁(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: (H₁(V,C) [;] (u,(H₁(V,C) .: ((pseudo_compl (V,C)),((StrongImpl (V,C)) [:] ((diff u),v)))))) . w [= v
then A3: w "\/" ((diff u) . w) = u by Lm5;
(H₁(V,C) [;] (u,(H₁(V,C) .: ((pseudo_compl (V,C)),((StrongImpl (V,C)) [:] ((diff u),v)))))) . w = H₁(V,C) . (u,((H₁(V,C) .: ((pseudo_compl (V,C)),((StrongImpl (V,C)) [:] ((diff u),v)))) . w)) by FUNCOP_1:53
.= u "/\" ((H₁(V,C) .: ((pseudo_compl (V,C)),((StrongImpl (V,C)) [:] ((diff u),v)))) . w) by LATTICES:def 2
.= u "/\" (H₁(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
.= (((diff u) . w) "/\" ((StrongImpl (V,C)) . (((diff u) . w),v))) "/\" ((pseudo_compl (V,C)) . w) by LATTICES:def 7 ;
then A4: (H₁(V,C) [;] (u,(H₁(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 (H₁(V,C) [;] (u,(H₁(V,C) .: ((pseudo_compl (V,C)),((StrongImpl (V,C)) [:] ((diff u),v)))))) . w [= v by A4, LATTICES:7; :: thesis: verum

end;

u "/\" H₂(u,v) = FinJoin ((SUB u),(H₁(V,C) [;] (u,(H₁(V,C) .: ((pseudo_compl (V,C)),((StrongImpl (V,C)) [:] ((diff u),v))))))) by LATTICE2:66;
hence u "/\" H₂(u,v) [= v by A1, LATTICE2:54; :: thesis: for w being Element of (SubstLatt (V,C)) st u "/\" v [= w holds
v [= H₂(u,w)
let w be Element of (SubstLatt (V,C)); :: thesis: ( u "/\" v [= w implies v [= H₂(u,w) )
assume A5: u "/\" v [= w ; :: thesis: v [= H₂(u,w)
A6: v = FinJoin (v9,(Atom (V,C))) by Th19;
then A7: u "/\" v = FinJoin (v9,(H₁(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 [= H₂(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 [= H₂(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 [= H₂(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;
(H₁(V,C) [;] (u,(Atom (V,C)))) . a [= w by A7, A5, A11, LATTICE2:31;
then H₁(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) = H₁(V,C) . (((pseudo_compl (V,C)) . v9),(((StrongImpl (V,C)) [:] ((diff u),w)) . v9)) by LATTICES:def 2
.= (H₁(V,C) .: ((pseudo_compl (V,C)),((StrongImpl (V,C)) [:] ((diff u),w)))) . v9 by FUNCOP_1:37 ;
then (Atom (V,C)) . a [= (H₁(V,C) .: ((pseudo_compl (V,C)),((StrongImpl (V,C)) [:] ((diff u),w)))) . v9 by A14, A15, FILTER_0:7;
hence (Atom (V,C)) . a [= H₂(u,w) by A8, LATTICE2:29; :: thesis: verum

end;

hence v [= H₂(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 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 end;