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;

{} 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

hence
Bottom (NormForm A) = {}
by LATTICE2:14; :: thesis: verumlet 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;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