let A be set ; :: thesis: for u, v being Element of 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 ; :: thesis: u => v = FinJoin (SUB u),(the L_meet of (NormForm A) .: (pseudo_compl A),((StrongImpl A) [:] (diff u),v))
deffunc H₃( Element of , Element of ) -> 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 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 8; :: thesis: verum