set G = NormForm A;

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

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

proof

thus
NormForm A is lower-bounded
:: thesis: verum
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;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

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_{1} being Element of the carrier of (NormForm A) holds

( e "/\" b_{1} = e & b_{1} "/\" 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;reconsider e = E as Element of (NormForm A) by Def12;

take e ; :: according to LATTICES:def 13 :: thesis: for b

( e "/\" b

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