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_{3}( Element of (NormForm A), Element of (NormForm A)) -> Element of the carrier of (NormForm A) = FinJoin ((SUB $1),(H_{2}(A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff $1),$2)))));

( u "/\" H_{3}(u,v) [= v & ( for w being Element of (NormForm A) st u "/\" w [= v holds

w [= H_{3}(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

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

( u "/\" H

w [= H

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