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, u' = u as Element of SubstitutionSet V,C by Def4;
thus Z "/\" u = mi (z ^ u') by Def4
.= mi (u' ^ z) by Th3
.= mi u' by Th4
.= u by Th11 ; :: thesis: verum

end;

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