let V, C be set ; :: thesis: for a, b being Element of (SubstLatt V,C) holds a "/\" b = b "/\" a
let a, b be Element of (SubstLatt V,C); :: thesis: a "/\" b = b "/\" a
reconsider a' = a, b' = b as Element of SubstitutionSet V,C by Def4;
a "/\" b = mi (a' ^ b') by Def4
.= mi (b' ^ a') by Th3
.= b "/\" a by Def4 ;
hence a "/\" b = b "/\" a ; :: thesis: verum