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 :: 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
.= u by Th11 ; :: thesis: verum
end;
hence Bottom (SubstLatt (V,C)) = {} by LATTICE2:14; :: thesis: verum