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 7 :: thesis: ex b₁ being Element of the carrier of (SubstLatt V,C) st
( p "/\" b₁ [= q & ( for b₂ being Element of the carrier of (SubstLatt V,C) holds
( not p "/\" b₂ [= q or b₂ [= b₁ ) ) )
take r = FinJoin (SUB p),(H₁(V,C) .: (pseudo_compl V,C),((StrongImpl V,C) [:] (diff p),q)); :: thesis: ( p "/\" r [= q & ( for b₁ being Element of the carrier of (SubstLatt V,C) holds
( not p "/\" b₁ [= q or b₁ [= r ) ) )
thus ( p "/\" r [= q & ( for r1 being Element of (SubstLatt V,C) st p "/\" r1 [= q holds
r1 [= r ) ) by Lm10; :: thesis: verum