set G = NormForm A;
thus NormForm A is distributive :: thesis: NormForm A is lower-bounded

proof

let u, v, w be Element of (NormForm A); :: according to LATTICES:def 11 :: thesis: u "/\" (v "\/" w) = (u "/\" v) "\/" (u "/\" w)
reconsider K = u, L = v, M = w as Element of Normal_forms_on A by Def12;
thus u "/\" (v "\/" w) = the L_meet of (NormForm A) . (K,( the L_join of (NormForm A) . (L,M)))
.= (u "/\" v) "\/" (u "/\" w) by Lm15 ; :: thesis: verum

end;

thus NormForm A is lower-bounded :: thesis: verum

proof

reconsider E = {} as Element of Normal_forms_on A by Lm4;
reconsider e = E as Element of (NormForm A) by Def12;
take e ; :: according to LATTICES:def 13 :: thesis: for b₁ being Element of the carrier of (NormForm A) holds
( e "/\" b₁ = e & b₁ "/\" e = e )
let u be Element of (NormForm A); :: thesis: ( e "/\" u = e & u "/\" e = e )
reconsider K = u as Element of Normal_forms_on A by Def12;
A1: e "\/" u = mi (E \/ K) by Def12
.= u by Th42 ;
then u "/\" e = e by LATTICES:def 9;
hence ( e "/\" u = e & u "/\" e = e ) by A1, LATTICES:def 9; :: thesis: verum

end;