let A be set ; :: thesis: NormForm A is implicative

let p, q be Element of (NormForm A); :: according to FILTER_0:def 6 :: thesis: ex b_{1} being Element of the carrier of (NormForm A) st

( p "/\" b_{1} [= q & ( for b_{2} being Element of the carrier of (NormForm A) holds

( not p "/\" b_{2} [= q or b_{2} [= b_{1} ) ) )

take r = FinJoin ((SUB p),(H_{2}(A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff p),q))))); :: thesis: ( p "/\" r [= q & ( for b_{1} being Element of the carrier of (NormForm A) holds

( not p "/\" b_{1} [= q or b_{1} [= r ) ) )

thus ( p "/\" r [= q & ( for r1 being Element of (NormForm A) st p "/\" r1 [= q holds

r1 [= r ) ) by Lm9; :: thesis: verum

let p, q be Element of (NormForm A); :: according to FILTER_0:def 6 :: thesis: ex b

( p "/\" b

( not p "/\" b

take r = FinJoin ((SUB p),(H

( not p "/\" b

thus ( p "/\" r [= q & ( for r1 being Element of (NormForm A) st p "/\" r1 [= q holds

r1 [= r ) ) by Lm9; :: thesis: verum