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