let A be set ; :: thesis: for u, v being Element of (NormForm A) holds u => v = FinJoin ((SUB u),( the L_meet of (NormForm A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff u),v)))))
let u, v be Element of (NormForm A); :: thesis: u => v = FinJoin ((SUB u),( the L_meet of (NormForm A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff u),v)))))
deffunc H₃( Element of (NormForm A), Element of (NormForm A)) -> Element of the carrier of (NormForm A) = FinJoin ((SUB $1),(H₂(A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff $1),$2)))));
( u "/\" H₃(u,v) [= v & ( for w being Element of (NormForm A) st u "/\" w [= v holds
w [= H₃(u,v) ) ) by Lm9;
hence u => v = FinJoin ((SUB u),( the L_meet of (NormForm A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff u),v))))) by FILTER_0:def 7; :: thesis: verum