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₁ being Element of the carrier of (NormForm A) st
( p "/\" b₁ [= q & ( for b₂ being Element of the carrier of (NormForm A) holds
( not p "/\" b₂ [= q or b₂ [= b₁ ) ) )
take r = FinJoin ((SUB p),(H₂(A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff p),q))))); :: thesis: ( p "/\" r [= q & ( for b₁ being Element of the carrier of (NormForm A) holds
( not p "/\" b₁ [= q or b₁ [= r ) ) )
thus ( p "/\" r [= q & ( for r1 being Element of (NormForm A) st p "/\" r1 [= q holds
r1 [= r ) ) by Lm9; :: thesis: verum