let N be antisymmetric with_infima RelStr ; :: thesis: 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; :: thesis: ( N is transitive implies (n1 "/\" n2) "/\" n3 = n1 "/\" (n2 "/\" n3) )
assume A1: N is transitive ; :: thesis: (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;
now :: thesis: for n4 being Element of N st n4 <= n1 & n4 <= n2 "/\" n3 holds
n4 <= (n1 "/\" n2) "/\" n3
let n4 be Element of N; :: thesis: ( n4 <= n1 & n4 <= n2 "/\" n3 implies n4 <= (n1 "/\" n2) "/\" n3 )
assume that
A10: n4 <= n1 and
A11: n4 <= n2 "/\" n3 ; :: thesis: n4 <= (n1 "/\" n2) "/\" n3
A12: n4 <= n2 by A1, A4, A11, ORDERS_2:3;
A13: n4 <= n3 by A1, A5, A11, ORDERS_2:3;
n4 <= n1 "/\" n2 by A10, A12, Lm2;
hence n4 <= (n1 "/\" n2) "/\" n3 by A13, Lm2; :: thesis: verum
end;
hence (n1 "/\" n2) "/\" n3 = n1 "/\" (n2 "/\" n3) by A8, A9, Def14; :: thesis: verum