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

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:24; :: thesis: verum