let N be antisymmetric with_infima RelStr ; for n1, n2, n3 being Element of N st N is transitive holds
(n1 "/\" n2) "/\" n3 = n1 "/\" (n2 "/\" n3)
let n1, n2, n3 be Element of N; ( N is transitive implies (n1 "/\" n2) "/\" n3 = n1 "/\" (n2 "/\" n3) )
assume A1:
N is transitive
; (n1 "/\" n2) "/\" n3 = n1 "/\" (n2 "/\" n3)
A2:
n1 "/\" n2 <= n1
by Lm2;
A3:
n1 "/\" n2 <= n2
by Lm2;
A4:
n2 "/\" n3 <= n2
by Lm2;
A5:
n2 "/\" n3 <= n3
by Lm2;
A6:
(n1 "/\" n2) "/\" n3 <= n1 "/\" n2
by Lm2;
A7:
(n1 "/\" n2) "/\" n3 <= n3
by Lm2;
A8:
(n1 "/\" n2) "/\" n3 <= n1
by A1, A2, A6, ORDERS_2:3;
(n1 "/\" n2) "/\" n3 <= n2
by A1, A3, A6, ORDERS_2:3;
then A9:
(n1 "/\" n2) "/\" n3 <= n2 "/\" n3
by A7, Lm2;
hence
(n1 "/\" n2) "/\" n3 = n1 "/\" (n2 "/\" n3)
by A8, A9, Def14; verum