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 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;
now :: thesis: for u4 being Element of V st u1 <= u4 & u2 "\/" u3 <= u4 holds
(u1 "\/" u2) "\/" u3 <= u4
let u4 be Element of V; :: 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 A1, A4, A11, ORDERS_2:3;
A13: u3 <= u4 by A1, A5, A11, ORDERS_2:3;
u1 "\/" u2 <= u4 by A10, A12, Lm1;
hence (u1 "\/" u2) "\/" u3 <= u4 by A13, Lm1; :: thesis: verum
end;
hence (u1 "\/" u2) "\/" u3 = u1 "\/" (u2 "\/" u3) by A8, A9, Def13; :: thesis: verum