let V be set ; :: thesis: 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))
let C be finite set ; :: thesis: 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))
let u, v be Element of (SubstLatt V,C); :: thesis: u => v = FinJoin (SUB u),(the L_meet of (SubstLatt V,C) .: (pseudo_compl V,C),((StrongImpl V,C) [:] (diff u),v))
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));
A1: for w being Element of (SubstLatt V,C) st u "/\" w [= v holds
w [= H₂(u,v) by Lm10;
u "/\" H₂(u,v) [= v by Lm10;
hence u => v = FinJoin (SUB u),(the L_meet of (SubstLatt V,C) .: (pseudo_compl V,C),((StrongImpl V,C) [:] (diff u),v)) by A1, FILTER_0:def 8; :: thesis: verum