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 a' = a, b' = b as Element of SubstitutionSet V,C by Def4;
a "\/" b = mi (b' \/ a') by Def4
.= b "\/" a by Def4 ;
hence a "\/" b = b "\/" a ; :: thesis: verum