let A be set ; 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); u => v = FinJoin ((SUB u),( the L_meet of (NormForm A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff u),v)))))
deffunc H3( Element of (NormForm A), Element of (NormForm A)) -> Element of the carrier of (NormForm A) = FinJoin ((SUB $1),(H2(A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff $1),$2)))));
( u "/\" H3(u,v) [= v & ( for w being Element of (NormForm A) st u "/\" w [= v holds
w [= H3(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; verum