let A be set ; :: thesis: for a, b being Element of (NormForm A) holds (a "/\" b) "\/" b = b

let a, b be Element of (NormForm A); :: thesis: (a "/\" b) "\/" b = b

reconsider a9 = a, b9 = b as Element of Normal_forms_on A by Def12;

set G = NormForm A;

thus (a "/\" b) "\/" b = the L_join of (NormForm A) . (( the L_meet of (NormForm A) . (a9,b9)),b9)

.= b by Lm11 ; :: thesis: verum

let a, b be Element of (NormForm A); :: thesis: (a "/\" b) "\/" b = b

reconsider a9 = a, b9 = b as Element of Normal_forms_on A by Def12;

set G = NormForm A;

thus (a "/\" b) "\/" b = the L_join of (NormForm A) . (( the L_meet of (NormForm A) . (a9,b9)),b9)

.= b by Lm11 ; :: thesis: verum