let V be antisymmetric with_suprema RelStr ; 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; ( V is transitive implies (u1 "\/" u2) "\/" u3 = u1 "\/" (u2 "\/" u3) )
assume A1:
V is transitive
; (u1 "\/" u2) "\/" u3 = u1 "\/" (u2 "\/" u3)
A2:
u1 <= u1 "\/" u2
by Lm1;
A3:
u2 <= u1 "\/" u2
by Lm1;
A4:
u2 <= u2 "\/" u3
by Lm1;
A5:
u3 <= u2 "\/" u3
by Lm1;
A6:
u1 "\/" u2 <= (u1 "\/" u2) "\/" u3
by Lm1;
A7:
u3 <= (u1 "\/" u2) "\/" u3
by Lm1;
A8:
u1 <= (u1 "\/" u2) "\/" u3
by A1, A2, A6, ORDERS_2:3;
u2 <= (u1 "\/" u2) "\/" u3
by A1, A3, A6, ORDERS_2:3;
then A9:
u2 "\/" u3 <= (u1 "\/" u2) "\/" u3
by A7, Lm1;
hence
(u1 "\/" u2) "\/" u3 = u1 "\/" (u2 "\/" u3)
by A8, A9, Def13; verum