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 a' = a, b' = b as Element of Normal_forms_on A by Def14;
thus a "/\" (a "\/" b) = the L_join of (NormForm A) . (the L_meet of (NormForm A) . a',a'),(the L_meet of (NormForm A) . a',b') by Lm15
.= the L_join of (NormForm A) . (mi (a' ^ a')),(the L_meet of (NormForm A) . a',b') by Def14
.= the L_join of (NormForm A) . (mi a'),(the L_meet of (NormForm A) . a',b') by Th79
.= a "\/" (a "/\" b) by Th66
.= (a "/\" b) "\/" a by Lm9
.= (b "/\" a) "\/" a by Lm13
.= a by Lm12 ; :: thesis: verum