let A be set ; :: thesis: for u, v being Element of (NormForm A) holds (diff u) . v [= u
let u, v be Element of (NormForm A); :: thesis: (diff u) . v [= u
(diff u) . v = u \ v by Def11;
then for a being Element of DISJOINT_PAIRS A st a in (diff u) . v holds
ex b being Element of DISJOINT_PAIRS A st
( b in u & b c= a ) ;
hence (diff u) . v [= u by Lm3; :: thesis: verum