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

set G = NormForm A;

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

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

a "/\" (b "/\" c) = the L_meet of (NormForm A) . (a,(mi (b9 ^ c9))) by Def12

.= mi (a9 ^ (mi (b9 ^ c9))) by Def12

.= mi (a9 ^ (b9 ^ c9)) by Th51

.= mi ((a9 ^ b9) ^ c9) by Th52

.= mi ((mi (a9 ^ b9)) ^ c9) by Th50

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

.= (a "/\" b) "/\" c by Def12 ;

hence a "/\" (b "/\" c) = (a "/\" b) "/\" c ; :: thesis: verum

set G = NormForm A;

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

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

a "/\" (b "/\" c) = the L_meet of (NormForm A) . (a,(mi (b9 ^ c9))) by Def12

.= mi (a9 ^ (mi (b9 ^ c9))) by Def12

.= mi (a9 ^ (b9 ^ c9)) by Th51

.= mi ((a9 ^ b9) ^ c9) by Th52

.= mi ((mi (a9 ^ b9)) ^ c9) by Th50

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

.= (a "/\" b) "/\" c by Def12 ;

hence a "/\" (b "/\" c) = (a "/\" b) "/\" c ; :: thesis: verum