let V be antisymmetric with_suprema RelStr ; :: thesis: for u1, u2, u3 being Element of V st V is transitive holds
(u1 "\/" u2) "\/" u3 = u1 "\/" (u2 "\/" u3)
let u1, u2, u3 be Element of V; :: thesis: ( V is transitive implies (u1 "\/" u2) "\/" u3 = u1 "\/" (u2 "\/" u3) )
assume A1: V is transitive ; :: thesis: (u1 "\/" u2) "\/" u3 = u1 "\/" (u2 "\/" u3)
A2: ( u1 <= u1 "\/" u2 & u2 <= u1 "\/" u2 & u2 <= u2 "\/" u3 & u3 <= u2 "\/" u3 & u1 "\/" u2 <= (u1 "\/" u2) "\/" u3 & u3 <= (u1 "\/" u2) "\/" u3 ) by Lm1;
then A3: ( u1 <= (u1 "\/" u2) "\/" u3 & u2 <= (u1 "\/" u2) "\/" u3 ) by A1, ORDERS_2:26;
then A4: u2 "\/" u3 <= (u1 "\/" u2) "\/" u3 by A2, Lm1;

now

let u4 be Element of V; :: thesis: ( u1 <= u4 & u2 "\/" u3 <= u4 implies (u1 "\/" u2) "\/" u3 <= u4 )
assume A5: ( u1 <= u4 & u2 "\/" u3 <= u4 ) ; :: thesis: (u1 "\/" u2) "\/" u3 <= u4
then A6: ( u2 <= u4 & u3 <= u4 ) by A1, A2, ORDERS_2:26;
then u1 "\/" u2 <= u4 by A5, Lm1;
hence (u1 "\/" u2) "\/" u3 <= u4 by A6, Lm1; :: thesis: verum

end;

hence (u1 "\/" u2) "\/" u3 = u1 "\/" (u2 "\/" u3) by A3, A4, Def13; :: thesis: verum