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 7; :: thesis: verum