let A be set ; :: thesis: for a, b being Element of (NormForm A) holds a "/\" b = b "/\" a
set G = NormForm A;
let a, b be Element of (NormForm A); :: thesis: a "/\" b = b "/\" a
reconsider a9 = a, b9 = b as Element of Normal_forms_on A by Def14;
a "/\" b = mi (a9 ^ b9) by Def14
.= mi (b9 ^ a9) by Th72
.= b "/\" a by Def14 ;
hence a "/\" b = b "/\" a ; :: thesis: verum