let V, C be set ; :: thesis: Bottom (SubstLatt V,C) = {}
{} in SubstitutionSet V,C by Th1;
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
.= u by Th11 ; :: thesis: verum

end;

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