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

set G = NormForm A;

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

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

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

.= the L_join of (NormForm A) . ((mi (a9 ^ a9)),( the L_meet of (NormForm A) . (a9,b9))) by Def12

.= the L_join of (NormForm A) . ((mi a9),( the L_meet of (NormForm A) . (a9,b9))) by Th55

.= a "\/" (a "/\" b) by Th42

.= (a "/\" b) "\/" a by Lm9

.= (b "/\" a) "\/" a by Lm13

.= a by Lm12 ; :: thesis: verum

set G = NormForm A;

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

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

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

.= the L_join of (NormForm A) . ((mi (a9 ^ a9)),( the L_meet of (NormForm A) . (a9,b9))) by Def12

.= the L_join of (NormForm A) . ((mi a9),( the L_meet of (NormForm A) . (a9,b9))) by Th55

.= a "\/" (a "/\" b) by Th42

.= (a "/\" b) "\/" a by Lm9

.= (b "/\" a) "\/" a by Lm13

.= a by Lm12 ; :: thesis: verum