let A be set ; :: thesis: Bottom (NormForm A) = {}
{} in Normal_forms_on A by Lm4;
then reconsider Z = {} as Element of (NormForm A) by Def12;

now :: thesis: for u being Element of (NormForm A) holds Z "\/" u = u

let u be Element of (NormForm A); :: thesis: Z "\/" u = u
reconsider z = Z, u9 = u as Element of Normal_forms_on A by Def12;
thus Z "\/" u = mi (z \/ u9) by Def12
.= u by Th42 ; :: thesis: verum

end;

hence Bottom (NormForm A) = {} by LATTICE2:14; :: thesis: verum