let L be GAD_Lattice; ( L is join-commutative implies for u1, u2, u3 being Element of L holds (u1 "\/" u2) "\/" u3 = u1 "\/" (u2 "\/" u3) )
assume Z0:
L is join-commutative
; for u1, u2, u3 being Element of L holds (u1 "\/" u2) "\/" u3 = u1 "\/" (u2 "\/" u3)
let u1, u2, u3 be Element of L; (u1 "\/" u2) "\/" u3 = u1 "\/" (u2 "\/" u3)
Z1:
for x, y being Element of L holds
( ex_lub_of x,y & x "\/" y = lub (x,y) )
A2:
u1 [= u1 "\/" u2
by Lm1, Z0;
A3:
u2 [= u1 "\/" u2
by Lm1, Z0;
A4:
u2 [= u2 "\/" u3
by Lm1, Z0;
A5:
u3 [= u2 "\/" u3
by Lm1, Z0;
A6:
u1 "\/" u2 [= (u1 "\/" u2) "\/" u3
by Lm1, Z0;
A7:
u3 [= (u1 "\/" u2) "\/" u3
by Lm1, Z0;
A8:
u1 [= (u1 "\/" u2) "\/" u3
by A2, A6, TransLat;
u2 [= (u1 "\/" u2) "\/" u3
by A3, A6, TransLat;
then A9:
u2 "\/" u3 [= (u1 "\/" u2) "\/" u3
by A7, Lm1, Z0;
S1:
( ex_lub_of u1,u2 "\/" u3 & u1 "\/" (u2 "\/" u3) = lub (u1,(u2 "\/" u3)) )
by Z1;
hence
(u1 "\/" u2) "\/" u3 = u1 "\/" (u2 "\/" u3)
by A8, A9, S1, DefLUB; verum