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