let V, C be set ; :: thesis: Top (SubstLatt (V,C)) = {{}}
{{}} in SubstitutionSet (V,C) by Th2;
then reconsider Z = {{}} as Element of (SubstLatt (V,C)) by Def4;

now :: thesis: for u being Element of (SubstLatt (V,C)) holds Z "/\" u = u

let u be Element of (SubstLatt (V,C)); :: thesis: Z "/\" u = u
reconsider z = Z, u9 = u as Element of SubstitutionSet (V,C) by Def4;
thus Z "/\" u = mi (z ^ u9) by Def4
.= mi (u9 ^ z) by Th3
.= mi u9 by Th4
.= u by Th11 ; :: thesis: verum

end;

hence Top (SubstLatt (V,C)) = {{}} by LATTICE2:16; :: thesis: verum