let L be GAD_Lattice; :: thesis: ( 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 ; :: thesis: for u1, u2, u3 being Element of L holds (u1 "\/" u2) "\/" u3 = u1 "\/" (u2 "\/" u3)
let u1, u2, u3 be Element of L; :: thesis: (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) )
proof
let x, y be Element of L; :: thesis: ( ex_lub_of x,y & x "\/" y = lub (x,y) )
x "\/" y = y "\/" x by Z0;
hence ( ex_lub_of x,y & x "\/" y = lub (x,y) ) by Th381i4; :: thesis: verum
end;
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;
now :: thesis: for u4 being Element of L st u1 [= u4 & u2 "\/" u3 [= u4 holds
(u1 "\/" u2) "\/" u3 [= u4
let u4 be Element of L; :: thesis: ( u1 [= u4 & u2 "\/" u3 [= u4 implies (u1 "\/" u2) "\/" u3 [= u4 )
assume that
A10: u1 [= u4 and
A11: u2 "\/" u3 [= u4 ; :: thesis: (u1 "\/" u2) "\/" u3 [= u4
A12: u2 [= u4 by A4, A11, TransLat;
A13: u3 [= u4 by A5, A11, TransLat;
u1 "\/" u2 [= u4 by A10, A12, Lm1, Z0;
hence (u1 "\/" u2) "\/" u3 [= u4 by A13, Lm1, Z0; :: thesis: verum
end;
hence (u1 "\/" u2) "\/" u3 = u1 "\/" (u2 "\/" u3) by A8, A9, S1, DefLUB; :: thesis: verum