let V be set ; :: thesis: for C being finite set
for u, v being Element of (SubstLatt (V,C)) holds (diff u) . v [= u
let C be finite set ; :: thesis: for u, v being Element of (SubstLatt (V,C)) holds (diff u) . v [= u
let u, v be Element of (SubstLatt (V,C)); :: thesis: (diff u) . v [= u
(diff u) . v = u \ v by Def7;
then for a being set st a in (diff u) . v holds
ex b being set st
( b in u & b c= a ) ;
hence (diff u) . v [= u by Lm8; :: thesis: verum