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 6 :: 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