let A be set ; :: thesis: for a, b being Element of holds (a "/\" b) "\/" b = b
let a, b be Element of ; :: thesis: (a "/\" b) "\/" b = b
reconsider a' = a, b' = b as Element of Normal_forms_on A by Def14;
set G = NormForm A;
thus (a "/\" b) "\/" b = the L_join of (NormForm A) . (the L_meet of (NormForm A) . a',b'),b'
.= b by Lm11 ; :: thesis: verum